Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity
2,072 Commits 14 Branches 9 Tags 76 MiB
Commit Graph

448 Commits

Author SHA1 Message Date
Burkhart Wolff de5c0fc6e2 added Isar-syntax for define_shortcut* 2020-12-22 08:07:19 +01:00
Burkhart Wolff 0e64608a58 enforcing shorter Definition* - style in examples (CC,CENELEC,...) 2020-12-02 09:32:48 +01:00
Burkhart Wolff 8771d8581b default class checking bug fixed; new attributes for default classes in ontological macros Definition* Theorem* Lemma* 2020-12-01 23:18:13 +01:00
Achim D. Brucker c11e68e3ea Bug fix: Definition environment. 2020-12-01 07:46:20 +00:00
Burkhart Wolff efeee1e863 Eliminated deprecated abstract class residuals; lifted Definition* to math_content. 2020-11-10 13:07:54 +01:00
Burkhart Wolff 2ecb62a80e added Lemma*, Theorem* and Definition* support. Bug: referencing does not work. 2020-11-04 15:55:43 +01:00
Burkhart Wolff 4ad06ce39a deactivated class check. 2020-11-04 14:25:14 +01:00
Burkhart Wolff da0f3e63f1 more steps to reform document macro mechanism 2020-11-04 13:13:24 +01:00
Achim D. Brucker 1ad81aff35 Added support for explicit abstract* command. 2020-11-03 21:47:05 +00:00
Achim D. Brucker 1129a0ed3e Added support for explicit author* command. 2020-11-03 21:43:55 +00:00
Burkhart Wolff bad7dfc2ef new set of macros : author* and abstract* --- not working yet 2020-11-03 19:00:33 +01:00
Burkhart Wolff fe8f63690d macro-arrangement ... 2020-11-02 18:30:40 +01:00
Burkhart Wolff e59ac46299 removed SI --- went to AFP 2020-11-02 14:32:41 +01:00
Burkhart Wolff aa1fed2440 sdf 2020-11-02 14:12:27 +01:00
Burkhart Wolff abd32a802d First Pass of Chap 4 - Added invariant syntax description, more semantic content 2020-10-26 12:27:33 +01:00
Achim D. Brucker a175871474 Improved definition of \ie and \eg. 2020-10-06 04:45:14 +01:00
Burkhart Wolff d655effcf8 pushup. 2020-09-22 16:47:05 +02:00
Burkhart Wolff 9956bbf062 pushup, stiluebungen. 2020-09-22 16:35:28 +02:00
Achim D. Brucker 137262890e Improved 'verbatim' output (removed generated %-signs). 2020-09-15 07:28:32 +01:00
Burkhart Wolff 77e3490477 ... 2020-09-09 16:56:19 +02:00
Achim D. Brucker 3eef2291e5 Integrated DOF-scholarly_paper-thm.sty. 2020-09-07 23:57:15 +01:00
Achim D. Brucker 7956a3009a Initial commit: style for providing theorem-like default environments. 2020-09-07 23:56:43 +01:00
Burkhart Wolff bb68be990b added wrapper to achims listings environments. 2020-08-28 12:49:28 +02:00
Burkhart Wolff 094281cf89 added wrapper to achims listings environments. 2020-08-28 12:42:20 +02:00
Burkhart Wolff d206bf9f7c shifted new env up into COL. Declared in the Frontmatter. 2020-08-27 15:54:51 +02:00
Burkhart Wolff 38ba8cace0 brought experiments with generic sub-text-element-environments into shape 2020-08-27 14:08:49 +02:00
Burkhart Wolff fef4243e45 added define_macro2 2020-08-27 10:13:52 +02:00
Burkhart Wolff b3ff21e210 introducing and testing of macros bindex and index. 2020-08-26 17:08:45 +02:00
Burkhart Wolff 41a1eaed44 added define_macros, corrections in 02_Background 2020-08-26 14:38:39 +02:00
Burkhart Wolff 00c4d15259 first feedback on Yakoubs CC 2020-08-26 11:48:25 +02:00
Burkhart Wolff 1dd07880ea inbtroduced shortcut interface. 2020-08-26 09:56:25 +02:00
Burkhart Wolff 7a768cfdeb versatile 2020-08-26 08:43:39 +02:00
Burkhart Wolff 338bb7d4a4 Code cleanup. 2020-08-25 11:59:10 +02:00
Burkhart Wolff a792cc79d2 was lucky to solve a deep bug in standard antiquotation evaluation inside text* soon. 2020-08-25 11:11:38 +02:00
Burkhart Wolff 8002ec31bb cleanups after discussion 2020-08-24 14:36:22 +02:00
Burkhart Wolff ff63b441b0 more on aop 2020-08-24 13:18:25 +02:00
Burkhart Wolff dbce392e8b experiments with latex generation for aoo presentation. 2020-08-24 12:11:30 +02:00
Burkhart Wolff 7cb6577797 solved presentation bug (brown) and eliminated some code dups 2020-08-24 11:33:32 +02:00
Burkhart Wolff d088d19f38 renamings - no reference to Iso which is possibly different 2020-08-24 09:40:56 +02:00
Burkhart Wolff 9a8b0c7c55 adapting Yakoubs Version on CC into our structure. Using our Definition setup. 2020-08-24 09:01:54 +02:00
Burkhart Wolff f35d498ad8 added stubs for CC project 2020-08-20 12:53:39 +02:00
Burkhart Wolff 1470776428 slight correction of the template, and addition of SML template instance in DOF-technical_report. Does not work for test-case in 05_Implementation (Commented out)
Isabelle_DOF/Isabelle_DOF/pipeline/head There was a failure building this commit Details
2020-06-24 13:11:26 +02:00
Burkhart Wolff ef93285ec7 added a little useful template generation command
Isabelle_DOF/Isabelle_DOF/pipeline/head There was a failure building this commit Details
2020-06-23 14:02:04 +02:00
Burkhart Wolff f5622c2f59 Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF 2020-06-23 11:22:41 +02:00
Burkhart Wolff af9e399f50 some experiments with OoOP and the code support presentations. 2020-06-23 11:22:33 +02:00
Achim D. Brucker 1c5bb85233 Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
Isabelle_DOF/Isabelle_DOF/pipeline/head There was a failure building this commit Details
2020-06-23 07:29:20 +01:00
Achim D. Brucker 81ee0d9bbb Bug fix: support for UTF8 characters in author's names. 2020-06-23 06:56:35 +01:00
Burkhart Wolff 016a9e6454 Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
Isabelle_DOF/Isabelle_DOF/pipeline/head There was a failure building this commit Details
2020-06-22 17:42:48 +02:00
Burkhart Wolff 7e2224859e mmm 2020-06-22 17:42:40 +02:00
Burkhart Wolff 4717925eea Zwischenzustand OoO Generation
Isabelle_DOF/Isabelle_DOF/pipeline/head There was a failure building this commit Details
2020-06-16 09:08:36 +02:00
Burkhart Wolff d86c713e37 first running study of OoO - Presentation
Isabelle_DOF/Isabelle_DOF/pipeline/head There was a failure building this commit Details
2020-06-12 16:36:54 +02:00
Burkhart Wolff 0f9b6731af replaced structure with legecy code: Pure_Syn_Ext.
Isabelle_DOF/Isabelle_DOF/pipeline/head There was a failure building this commit Details
2020-06-12 15:00:49 +02:00
Burkhart Wolff d2d908534d Small corrections
Isabelle_DOF/Isabelle_DOF/pipeline/head There was a failure building this commit Details
2020-05-20 14:55:49 +02:00
Burkhart Wolff 3c6eda2cbb Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF 2020-05-19 17:32:31 +02:00
Burkhart Wolff 9b0c2cdcd8 added support for defn, lem, thm short-calls. 2020-05-19 17:32:25 +02:00
Simon Foster 1839afa883 Added proofs that quantities from a real normed vector space 2020-05-15 13:55:11 +01:00
Burkhart Wolff fa931b45e2 re-localization of onto macros. Tested. 2020-04-23 18:30:46 +02:00
Burkhart Wolff 6f8cd88623 nitty gritties 2020-04-23 16:59:49 +02:00
Burkhart Wolff 8328626fa4 Restructuring library prep. 2020-04-23 16:08:05 +02:00
Burkhart Wolff 9496b535b7 restructuring Lib. Adaption LaTeX. Reorg COL. 2020-04-23 14:31:59 +02:00
Burkhart Wolff 2e0d88a3f7 restructuring of COL, scholarly_paper, etc. Facturong out Macros. 2020-04-22 15:31:47 +02:00
Achim D. Brucker c320b58dd3 Merge remote-tracking branch 'origin/Unreleased/Isabelle2020-RC4' 2020-04-21 08:37:59 +01:00
Burkhart Wolff 2e7513271b support along AMS style for mcc. 2020-04-14 14:48:16 +02:00
Burkhart Wolff 88d4b7674e support along AMS style for mcc. 2020-04-14 14:44:42 +02:00
Burkhart Wolff 6cf5708d93 added macro_def mechanism. Bug: Type qualification necessary 2020-04-12 21:11:54 +02:00
Achim D. Brucker fa25654db9 Merge branch 'master' into Unreleased/Isabelle2020-RC4 2020-04-10 20:26:34 +01:00
Burkhart Wolff e642243847 added macrodef - expand mechanism 2020-04-10 18:30:33 +02:00
Burkhart Wolff 0c4a5a5fea eliminating deprecated syntax 2020-04-09 23:58:58 +02:00
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