Burkhart Wolff
e98e945b53
debugging.
2020-04-09 20:56:12 +02:00
Burkhart Wolff
d82870d1a0
support for math_example into the Urschleim.
2020-04-09 18:12:14 +02:00
Burkhart Wolff
f1b376d4b6
added support for math_content-class in scholarly_paper in Knuth's Urschleim.
2020-04-09 17:25:09 +02:00
Burkhart Wolff
aa4e1acf84
Added invariants - and changes of invariant syntax.
...
Modified scholarly_paper onto wrt to future concepts
of referential semi_formal items (according to discussion
with Achim).
2020-04-08 23:29:15 +02:00
Achim D. Brucker
358be52b61
Updated Isabelle version.
2020-04-08 21:40:34 +01:00
Achim D. Brucker
0c41ee46bb
Port to Isabelle 2020 (tested with Isabelle 2020 RC4).
2020-04-08 13:12:17 +01:00
Achim D. Brucker
6ec427e716
Cleanup.
2020-04-08 10:51:27 +01:00
Simon Foster
4cba4bbdc8
Added some additional non-SI units
2020-03-20 16:50:01 +00:00
Simon Foster
4b605faa2d
Improved proof support. Added some proofs of the astronomical constants.
2020-03-20 10:29:49 +00:00
Simon Foster
31c0dd56e8
Some renaming, cleaning, and addition of astronomical units
2020-03-18 16:02:09 +00:00
Simon Foster
25f2c76f1b
Restructured the document into the ISQ and SI parts
2020-03-18 12:03:56 +00:00
Simon Foster
0c73aa1ce7
Commented on the relationship between units and quantities, and added several supporting definitions and types.
2020-03-13 16:10:51 +00:00
Simon Foster
cf10043680
A few more revisions and explanations.
2020-03-13 14:54:46 +00:00
Simon Foster
1e31cbb8a1
Some fixes and improvements for proof support
2020-03-13 12:06:57 +00:00
Simon Foster
6feaeee050
More refactoring. The mechanisation is now split conveniently into a quantity and unit part. Most of the technical foundations
...
can be found in the former.
2020-03-13 11:21:43 +00:00
Simon Foster
da74d4ecc4
Revision of the narrative in Dimensions and Quantities
2020-03-12 17:23:47 +00:00
Simon Foster
1ee0a1610f
Refactoring to better distinguish quantities and units, which are now distinct entities.
2020-03-12 11:11:30 +00:00
Simon Foster
75e62c7356
Added definition of a base unit
2020-03-12 09:25:40 +00:00
Simon Foster
3fa136ec72
A few additional properties and proofs
2020-02-25 15:42:53 +00:00
Burkhart Wolff
3c90e19d11
added lemma into sty; fresh discussion with ADB on scholarly_paper onto.
2020-02-25 12:38:59 +01:00
Burkhart Wolff
f505e6cb79
polishing.
2020-02-24 18:47:51 +01:00
Burkhart Wolff
493a6c5559
improved intro, improved global structure (TOC), normalized terminology.
2020-02-24 18:36:07 +01:00
Burkhart Wolff
17c64ea60b
smoothening text
2020-02-24 13:10:21 +01:00
Burkhart Wolff
db810d7d9a
first version LaTeX infrastructure
2020-02-24 12:51:33 +01:00
Burkhart Wolff
54d641a1cc
renamings for units, poslishing. SOme more documentation of key elements.
2020-02-23 19:46:49 +01:00
Burkhart Wolff
edcfd988d3
renamings for dimensions-2
2020-02-23 19:11:11 +01:00
Burkhart Wolff
ed439e3731
renamings for dimensions-2
2020-02-23 19:10:21 +01:00
Burkhart Wolff
3f4348825b
renamings for dimensions
2020-02-23 19:06:32 +01:00
Burkhart Wolff
77d6c2212f
first elements on SI
2020-02-23 18:36:59 +01:00
Burkhart Wolff
9035c46023
syntax and 1st level type-checking of invariants
2020-02-21 19:23:51 +01:00
Burkhart Wolff
cc98979f43
more on class_id synonyms
2020-02-21 16:33:28 +01:00
Burkhart Wolff
15e605a1e7
Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2020-02-21 15:40:13 +01:00
Burkhart Wolff
3faf3102ee
First version with some places where type_synonyms were used to identify doc_classes
2020-02-21 15:39:50 +01:00
Simon Foster
dd5f983d70
A few more prefixes
2020-02-20 20:09:45 +00:00
Simon Foster
e1d4079c0f
Renamed Unit to Dimension. Added several more definitions and results from the standard.
2020-02-20 19:58:43 +00:00
Burkhart Wolff
2599caed01
Deleting outdated experiments.
2020-02-20 17:15:29 +01:00
Burkhart Wolff
75b6baea53
minimal changes due to revisions
2020-02-20 17:12:38 +01:00
Burkhart Wolff
818b9c9b4c
Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2020-02-20 13:30:56 +01:00
Burkhart Wolff
9df43f0085
various changes of the DOF-core interface: read_cid. Preparations for type_synonyms for cids. (unfinished). Updated scholarly_paper onto
2020-02-20 13:30:51 +01:00
Simon Foster
c40088199c
Some tidying of the proof strategy and derived properties
2020-02-20 09:54:45 +00:00
Burkhart Wolff
1de90a23b2
Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2020-02-19 18:13:46 +01:00
Burkhart Wolff
5b0db2efb1
New Regrouping in the scholarly Onto + LaTeX support. Tested.
2020-02-19 18:13:33 +01:00
Simon Foster
240c10eb58
Factored out definitions, and added several additional units
2020-02-19 17:02:24 +00:00
Simon Foster
583637859a
Cleaning up the proof procedure, and additional algebraic laws
2020-02-19 13:59:47 +00:00
Simon Foster
b8e347b4c8
Removed the scalar product and associated class instantiations in favour of scaleQ
2020-02-18 20:31:05 +00:00
Simon Foster
c104f1e2b2
Added the the scaleQ function that should allow removal of the scalar product operator
2020-02-18 20:25:45 +00:00
Simon Foster
2c63ef07e9
Added core physical constants of the 2019 SI standard, dimensionless units, and various proof facilities for support.
2020-02-18 17:46:53 +00:00
Burkhart Wolff
5c303a7192
Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2020-02-17 23:08:03 +01:00
Burkhart Wolff
c5b5f994ef
added onto markup support for definitions and examples in scholarly_paper lncs style
2020-02-17 23:07:34 +01:00
Simon Foster
02eefef9d9
Revised the way that dimensions are encoded. Added some example physical constants.
2020-02-17 15:38:09 +00:00
Burkhart Wolff
fe8a6c5c87
refinements of the technical class; added the document antiquotation doc_class; some experiments in SI.
2020-02-13 11:17:20 +01:00
Simon Foster
9199bc3109
Split out SI units into several files, and began adapting proof automation
2020-02-10 12:03:51 +00:00
Burkhart Wolff
ec32ed0486
reasoning on SI equivalence
2020-02-10 11:38:23 +01:00
Burkhart Wolff
7899e4ee9a
reasoning on SI equivalence
2020-02-10 10:12:46 +01:00
Burkhart Wolff
1172f0f30a
Varous little changes, and attemps to improve example sections and proof support.
2020-02-05 14:00:59 +01:00
Achim D. Brucker
85af8bc3ed
Bug fix for older e-tex versions requireing reserveinsert.
2020-01-14 17:46:56 +00:00
Achim D. Brucker
97db02c61d
Bug fix: default ontology was always included, if if not needed or even conflicting.
2020-01-07 16:59:17 +00:00
Burkhart Wolff
727b53edb6
Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2019-12-17 13:25:52 +01:00
Burkhart Wolff
cb1ead378a
added new sections in CommentedIsabelle concerning definitions and internal proofs
2019-12-17 13:25:43 +01:00
Simon Foster
726ff605d7
Integrated record version of SI units, and fixed a few problems arising.
2019-12-11 15:54:41 +00:00
Achim D. Brucker
1c07c13a31
Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
2019-12-11 15:53:31 +00:00
Achim D. Brucker
0ad18b9e5b
\reserveinserts{} is only needed for older TeX installations and no longer supported on recent TeX versions.
2019-12-11 15:52:57 +00:00
Burkhart Wolff
f7f1a0d10d
hint to a dimension bug...
2019-12-10 10:46:06 +01:00
Burkhart Wolff
890eee8b24
first step to fusion SI
2019-12-09 14:50:34 +01:00
Burkhart Wolff
6135820127
Little improvements in examples and presentation.
2019-12-06 15:41:41 +01:00
Burkhart Wolff
aa0331ae13
refined shot reflecting discussion on tuesday afternoon
2019-11-19 18:48:26 +01:00
Burkhart Wolff
0d37763e02
refined shot reflecting discussion on tuesday afternoon
2019-11-19 18:25:02 +01:00
Burkhart Wolff
ca20a55cfb
added class invariant check_exercise_inv_1
2019-11-19 11:11:56 +01:00
Burkhart Wolff
c0812396de
implemented discussed onto-model for exams // except invariants
2019-11-18 20:55:43 +01:00
Burkhart Wolff
c8d87af2e6
intermediate stage for onto after discussion this morning.
2019-11-15 11:33:29 +01:00
Burkhart Wolff
b3540f8f45
Some elements
2019-11-15 05:15:32 +01:00
Burkhart Wolff
6a2a479699
intermediate stage for onto after discussion this morning.
2019-11-12 13:13:39 +01:00
Burkhart Wolff
33fd8a0f7b
startpunkt
2019-11-12 10:27:34 +01:00
Burkhart Wolff
a1941b2f15
startpunkt
2019-11-12 10:10:25 +01:00
Burkhart Wolff
cc787cb9f1
Added Fred's example on modifying the proof context for parsing.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-10-01 17:57:26 +02:00
Achim D. Brucker
b863a0178f
Define new TOCs only when used together with the KOMA-Script classes.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-09-21 15:21:34 +01:00
Achim D. Brucker
32e9c3f71c
Added version independent DOI.
2019-08-19 09:48:45 +01:00
Achim D. Brucker
c698a7a811
Added information on how to run Isabelle/DOF using Docker and added setup for documenting latest release.
Isabelle_DOF/Isabelle_DOF/v1.0.x%2FIsabelle2019 This commit looks good
Details
2019-08-18 14:05:00 +01:00
Achim D. Brucker
39919ad3e1
Fixed typo.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-08-17 16:43:40 +01:00
Achim D. Brucker
d6d9e1bb5c
New command "reflect_ML_exports" for loading ML exported code into Isabelle's ML environment using the Isabelle's virtual file system.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-08-17 16:31:27 +01:00
Achim D. Brucker
a30bf33d99
Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
Isabelle_DOF/Isabelle_DOF/master There was a failure building this commit
Details
2019-08-17 10:51:21 +01:00
Achim D. Brucker
ad0a3b293d
Removed outdated and unused file.
2019-08-17 10:50:43 +01:00
Achim D. Brucker
fdd9509eac
Remove and ignore autogenerated file.
Isabelle_DOF/Isabelle_DOF/master There was a failure building this commit
Details
2019-08-17 10:23:41 +01:00
Burkhart Wolff
dc15a31db6
removed awkward sentence.
2019-08-17 11:07:08 +02:00
Achim D. Brucker
c34b13ba2f
Reverted 7aefbde58b
.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-08-17 09:40:25 +01:00
Burkhart Wolff
7aefbde58b
typos, and a more general abstract.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-08-17 10:23:16 +02:00
Achim D. Brucker
60ebbbe12c
Updated license information.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-08-15 15:09:55 +01:00
Achim D. Brucker
6cd8cb098b
Updated license information.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-08-15 14:52:15 +01:00
Achim D. Brucker
22529362a1
Update version information during installation.
2019-08-15 14:37:04 +01:00
Burkhart Wolff
6e44230efb
Updated COL section ...
2019-08-15 11:30:42 +02:00
Burkhart Wolff
8a3622c125
Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-08-14 17:23:08 +02:00
Burkhart Wolff
b5fe2d9085
Solution to the assert - Bug : stronger checks in doc_class that reject correctly constructed, but lexically illegal long_names for doc_classes.
2019-08-14 17:22:55 +02:00
Achim D. Brucker
731ba1c1e4
Use Isabelle/DOF URL from config file.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-08-13 09:46:20 +01:00
Achim D. Brucker
b1d4abbf48
Introduced \dofurl.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-08-12 08:28:16 +01:00
Achim D. Brucker
f71706e67d
Renamed base url to artifact url.
2019-08-12 07:51:22 +01:00
Achim D. Brucker
332daa1ebb
Removed outdated and unsupported gen_sty_template.
2019-08-11 22:26:17 +01:00
Achim D. Brucker
6198602740
Moved \bibliographystyle{} to the top of the template to allow overriding it in preample.tex
2019-08-11 09:21:17 +01:00
Achim D. Brucker
5f692fa526
Fixed error message still refering to scholarly paper (instead of technical report) ontology.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-08-04 22:54:46 +01:00
Achim D. Brucker
6e6c4a81cb
Updated Isabelle/DOF repository URL.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-08-04 22:47:52 +01:00
Achim D. Brucker
e63e07cb1c
Improved autref configuration.
2019-08-04 18:11:48 +01:00
Achim D. Brucker
a7418304ed
Added support for \isabellefullversion and \isabelleurl.
2019-08-04 13:25:56 +01:00
Achim D. Brucker
5a532ec973
Use scrartcl as default LaTeX class.
2019-08-04 13:25:14 +01:00
Achim D. Brucker
df12a32624
Added missing space to warning messages.
2019-08-04 08:24:01 +01:00
Achim D. Brucker
abe4e8ef9a
Changed default ontology to scholarly_paper.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-08-03 22:06:44 +01:00
Achim D. Brucker
b0a845c2f1
Install internal styles into document-template folder so that they are not listed as ontologies.
2019-08-03 22:01:41 +01:00
Achim D. Brucker
9c7f6f6a28
Renamed DOF_mkroot to mkroot_DOF.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-08-03 21:36:06 +01:00
Achim D. Brucker
8c29055ec6
Moved version-related configuration into a .config file.
2019-08-03 21:32:40 +01:00
Achim D. Brucker
e1a16647ce
Restructured macros for release version and download URLs.
2019-08-03 16:02:54 +01:00
Achim D. Brucker
cef99fadc0
Added basic infrastructure for versions and URLs.
2019-08-02 20:07:32 +01:00
Achim D. Brucker
0c2e2869a7
Do not list subsubsections in TOC.
2019-08-02 11:12:59 +01:00
Achim D. Brucker
768bfea3b7
Replace <@> by @ in LaTeX files.
2019-08-01 20:43:33 +01:00
Achim D. Brucker
c8abf69d8d
Introduced \isabelleversion.
2019-07-28 20:46:20 +01:00
Achim D. Brucker
94fdf75627
Applied renaming: Paris-Sud to Paris-Saclay.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-07-28 12:01:58 +01:00
Achim D. Brucker
76c722b3bb
Updated chapter/section titles.
2019-07-28 10:56:04 +01:00
Achim D. Brucker
c43d844082
Updated page layout.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-07-27 20:16:28 +01:00
Achim D. Brucker
a433c6ba06
Improved support for SRAC, EC, assumption, and hypthesis.
2019-07-27 19:05:10 +01:00
Achim D. Brucker
14a7bee506
Updated layout for SRACs and ECs and added table of SRACs/ECs.
2019-07-27 15:14:32 +01:00
Achim D. Brucker
db9afaaa49
Added frontmatter-environment for supporting configuration using hooks.
2019-07-27 15:11:43 +01:00
Achim D. Brucker
6b0ce07ef6
Added basic layout for SRACs and ECs.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-07-27 09:39:40 +01:00
Achim D. Brucker
d0306e62bc
Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-07-23 15:31:03 +01:00
Achim D. Brucker
7093fb523c
Fixed URL style.
2019-07-23 15:13:15 +01:00
Burkhart Wolff
97701d62d7
local improvements due to remarks of Frederic.
2019-07-23 15:26:48 +02:00
Achim D. Brucker
a6b3a6f44e
Initial commit.
2019-07-23 13:51:30 +01:00
Achim D. Brucker
c22824e617
Updted default layout for technical reports.
2019-07-21 16:45:50 +01:00
Achim D. Brucker
5e59cf737b
Updated descriptions of templates.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
2019-07-21 10:13:51 +01:00
Achim D. Brucker
df3e3bd3c3
Updated copyright information.
2019-07-21 09:58:41 +01:00
Achim D. Brucker
0c158450b6
Updated copyright information.
2019-07-21 09:57:51 +01:00
Achim D. Brucker
ee574cdf99
Removed non-supported sty-file generation.
2019-07-21 09:43:36 +01:00
Achim D. Brucker
6fd22a071f
Resolved naming inconsistency (mathex_onto vs. math_exam).
Isabelle_DOF/Isabelle_DOF/master There was a failure building this commit
Details
2019-07-20 21:51:55 +01:00
Achim D. Brucker
8953f37629
Large directory restructuring.
...
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
This commit restructures the file hierarchy:
1) implementation is moved into src/ directory to clean up
the main directory and to make it easier for users to
find the README.md.
2) ontologies (both, the Isabelle-part and the LaTeX-part) are
now structured into directories.
2019-07-20 21:12:40 +01:00