Commit Graph

70 Commits

Author SHA1 Message Date
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
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 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 338bb7d4a4 Code cleanup. 2020-08-25 11:59:10 +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 7e2224859e mmm 2020-06-22 17:42:40 +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 9b0c2cdcd8 added support for defn, lem, thm short-calls. 2020-05-19 17:32:25 +02: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 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
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 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 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
Burkhart Wolff 5b0db2efb1 New Regrouping in the scholarly Onto + LaTeX support. Tested. 2020-02-19 18:13:33 +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
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
Achim D. Brucker 85af8bc3ed Bug fix for older e-tex versions requireing reserveinsert. 2020-01-14 17:46:56 +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 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