Commit Graph

333 Commits

Author SHA1 Message Date
Burkhart Wolff 41a1eaed44 added define_macros, corrections in 02_Background 2020-08-26 14:38:39 +02:00
Burkhart Wolff 1dd07880ea inbtroduced shortcut interface. 2020-08-26 09:56:25 +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 f239b36b49 Reworked textually abstract, intro, background. Eliminate \emph 2020-08-25 09:17:36 +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) 2020-06-24 13:11:26 +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
Burkhart Wolff 7e2224859e mmm 2020-06-22 17:42:40 +02:00
Burkhart Wolff 9b0c2cdcd8 added support for defn, lem, thm short-calls. 2020-05-19 17:32:25 +02:00
Achim D. Brucker 640ba5db6d Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF 2020-05-03 14:59:01 +01:00
Achim D. Brucker 3de76c8023 Improved description of TeX requirements. 2020-05-03 14:58:43 +01:00
Burkhart Wolff 8328626fa4 Restructuring library prep. 2020-04-23 16:08:05 +02:00
Achim D. Brucker fa25654db9 Merge branch 'master' into Unreleased/Isabelle2020-RC4 2020-04-10 20:26:34 +01:00
Burkhart Wolff 0c4a5a5fea eliminating deprecated syntax 2020-04-09 23:58:58 +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
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
Achim D. Brucker 85af8bc3ed Bug fix for older e-tex versions requireing reserveinsert. 2020-01-14 17:46:56 +00:00
Burkhart Wolff 80f7a73b88 added a publisher to avoid a warning 2020-01-14 18:16:31 +01: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
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 cc787cb9f1 Added Fred's example on modifying the proof context for parsing. 2019-10-01 17:57:26 +02:00
Achim D. Brucker 750a176cd1 Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF 2019-08-19 09:49:08 +01:00
Achim D. Brucker 32e9c3f71c Added version independent DOI. 2019-08-19 09:48:45 +01:00
Burkhart Wolff a4aade4ffa merge with better conclusion of commented isa 2019-08-19 10:14:07 +02:00
Achim D. Brucker d0b183af79 Improved docker run command. 2019-08-18 18:02:54 +01:00
Achim D. Brucker c698a7a811 Added information on how to run Isabelle/DOF using Docker and added setup for documenting latest release. 2019-08-18 14:05:00 +01:00
Achim D. Brucker 1d2f7a808f Cleanup. 2019-08-18 13:57:51 +01:00
Achim D. Brucker 68a5bbfc82 Fixed typo. 2019-08-17 23:27:04 +01:00
Burkhart Wolff 242664e6fd Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF 2019-08-17 11:19:30 +02:00
Burkhart Wolff f7d7dd6d23 changed awkward sentences. 2019-08-17 11:19:12 +02:00
Achim D. Brucker 982bd0c5fb Updated refernce to SEFM paper. 2019-08-17 10:15:04 +01:00
Burkhart Wolff e6c6592143 Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF 2019-08-17 11:07:22 +02:00
Burkhart Wolff dc15a31db6 removed awkward sentence. 2019-08-17 11:07:08 +02:00
Achim D. Brucker 679408cfed Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF 2019-08-17 10:02:36 +01:00
Achim D. Brucker 4692201cb0 Normalized BibTeX keys. 2019-08-17 10:02:13 +01:00
Burkhart Wolff b707eff08d bug in article class. 2019-08-17 10:48:15 +02:00
Achim D. Brucker c92376871c Fixes spacing. 2019-08-17 09:46:17 +01:00
Burkhart Wolff f649f08c5e adding LNCS number. 2019-08-17 10:37:07 +02:00
Burkhart Wolff 3f4fb48602 clarifying some sentences in intro. 2019-08-17 10:32:56 +02:00
Burkhart Wolff 7aefbde58b typos, and a more general abstract. 2019-08-17 10:23:16 +02:00
Achim D. Brucker 60ebbbe12c Updated license information. 2019-08-15 15:09:55 +01:00
Achim D. Brucker 6cd8cb098b Updated license information. 2019-08-15 14:52:15 +01:00
Achim D. Brucker 1f6149b0c0 Removed outdated stuff that never should have been comitted in the first place. 2019-08-15 13:46:20 +01:00
Achim D. Brucker 59c6a1304b Removed outdated stuff that never should have been comitted in the first place. 2019-08-15 13:45:56 +01:00
Achim D. Brucker 618997f34c Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF 2019-08-15 13:44:32 +01:00
Achim D. Brucker 8eb233e6eb Improved layout. 2019-08-15 13:31:16 +01:00
Burkhart Wolff 4d5fce3f1e older files. Flesh out useful stuff and eliminate the rest if necessary 2019-08-15 13:57:43 +02:00
Burkhart Wolff 1da0433451 improved layout 2019-08-15 11:44:29 +02:00
Burkhart Wolff 6414e1e568 improved layout 2019-08-15 11:40:47 +02:00
Burkhart Wolff ed1143cae3 resolved conflict[D 2019-08-15 11:32:29 +02:00
Burkhart Wolff 6e44230efb Updated COL section ... 2019-08-15 11:30:42 +02:00
Achim D. Brucker 13a92fcf34 Minor layout improvements. 2019-08-14 20:04:37 +01:00
Burkhart Wolff 8a3622c125 Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF 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 2b2826a83f Removed no longer required packages. 2019-08-13 09:32:15 +01:00
Achim D. Brucker d00cf8d4c3 Use default tt font instead of beramono. 2019-08-13 09:24:32 +01:00
Achim D. Brucker 40bb39c89c Moved loading of listings-package into lstisadof-manual.sty. 2019-08-13 09:21:33 +01:00
Achim D. Brucker e2a752ab55 Removed no longer required inpara-package. 2019-08-13 09:18:47 +01:00
Achim D. Brucker 803fea739e Fixed link to the Isabelle website. 2019-08-13 08:55:57 +01:00
Achim D. Brucker cb91c97028 Configured secnumdepth to not number paragraphs and subsubsections. 2019-08-13 08:55:43 +01:00
Achim D. Brucker 687fe0b61c Fixed typo. 2019-08-12 08:34:35 +01:00
Achim D. Brucker 17354942c2 Fixed typo. 2019-08-12 08:33:17 +01:00
Achim D. Brucker b1d4abbf48 Introduced \dofurl. 2019-08-12 08:28:16 +01:00
Achim D. Brucker 4d33021936 Improved several BibTeX entries. 2019-08-11 18:46:04 +01:00
Achim D. Brucker 40dcf89df9 Section 5.6. 2019-08-11 18:06:13 +01:00
Achim D. Brucker a79bd85e14 Section 5.5. 2019-08-11 17:22:22 +01:00
Achim D. Brucker a77053dc9e Number subsubsections. 2019-08-11 17:21:29 +01:00
Achim D. Brucker 5940542b24 Section 5.4. 2019-08-11 17:12:38 +01:00
Achim D. Brucker e58f0b33d4 Section 5.3. 2019-08-11 17:03:26 +01:00
Achim D. Brucker 37f4ce73b0 Section 5.2. 2019-08-11 16:59:48 +01:00
Achim D. Brucker 02377de0d2 Section 5.1. 2019-08-11 16:52:56 +01:00
Achim D. Brucker 4f242c06ba Added description of \renewisadof and \provideisadof. 2019-08-11 15:36:54 +01:00
Achim D. Brucker e3286a6a25 Section 4.3. 2019-08-11 15:05:56 +01:00
Achim D. Brucker 88dda0a05b Finished section 4.2. 2019-08-10 23:25:22 +01:00
Achim D. Brucker 7bff41cfa8 Moved and revised COL description. 2019-08-10 23:06:35 +01:00
Achim D. Brucker 7c66be090a Removed example - not needed as we have Chapter 3 (and various examples in the actual distribution). 2019-08-10 22:00:15 +01:00
Achim D. Brucker 898656077f Improved introduction of chapter 4. 2019-08-10 21:51:23 +01:00
Achim D. Brucker a96223235c Fixed installer output. 2019-08-10 20:43:29 +01:00
Achim D. Brucker d1f0e4fb05 Section 4.2.3 and 4.2.4. 2019-08-10 18:57:30 +01:00
Achim D. Brucker 06aa37d2a9 Section 4.2.2. 2019-08-09 17:37:39 +01:00
Achim D. Brucker b920423212 Activate literal Isabelle style. 2019-08-08 10:40:23 +01:00
Achim D. Brucker f1a6b6c60f Section restructuring. 2019-08-07 09:04:53 +01:00
Achim D. Brucker ad1138ec95 Section 4.2.1. 2019-08-06 16:44:48 +01:00
Achim D. Brucker b063c06023 Revised Section 4.1. 2019-08-05 11:48:56 +01:00
Achim D. Brucker 551906a599 Added style guide section. 2019-08-05 11:05:19 +01:00
Achim D. Brucker 5be97e2797 Improved paragraph on availability. 2019-08-05 10:39:39 +01:00
Achim D. Brucker 6e6c4a81cb Updated Isabelle/DOF repository URL. 2019-08-04 22:47:52 +01:00
Achim D. Brucker c70dec328e Removed list of SRACs/ECs. 2019-08-04 22:39:32 +01:00
Achim D. Brucker e2dee5addb Updated install script output to include check for pdftex. 2019-08-04 22:31:52 +01:00
Achim D. Brucker ba91746367 Added note that some LaTeX class files require a manual installation by the user. 2019-08-04 21:16:25 +01:00
Achim D. Brucker d89b9c6d65 Revised Section 3.4 2019-08-04 20:34:22 +01:00
Achim D. Brucker 451da54e0e Revised Section 3.3 2019-08-04 20:06:45 +01:00
Achim D. Brucker f85b1878fe Revised Section 3.2 2019-08-04 18:15:30 +01:00
Achim D. Brucker d1cd301e6e Added paragraph describing the document setup. 2019-08-04 15:32:16 +01:00
Achim D. Brucker 03fa1ed5f7 Revised Section 3.1 2019-08-04 13:37:57 +01:00
Achim D. Brucker 657d9376b2 Support automatic line breaks for bash environment. 2019-08-04 13:26:20 +01:00
Achim D. Brucker 60c6782874 Improved layout. 2019-08-04 08:23:49 +01:00
Achim D. Brucker 9c7f6f6a28 Renamed DOF_mkroot to mkroot_DOF. 2019-08-03 21:36:06 +01:00
Achim D. Brucker 4040767d1a Reworked prompt setup for bash environment. 2019-08-03 16:03:22 +01:00
Achim D. Brucker 88231c6898 Cleanup. 2019-08-03 12:03:09 +01:00
Achim D. Brucker 5066281145 Fixed index de-reference for outer syntax. 2019-08-02 20:10:38 +01:00
Achim D. Brucker 9c8365d1d0 Added home directory prompt. 2019-08-02 20:07:59 +01:00
Achim D. Brucker 3726304c9d Improved background sections and updated references to it. 2019-08-02 18:56:20 +01:00
Achim D. Brucker 080da57cb9 Fixed printing of bfindex. 2019-08-02 18:39:15 +01:00
Achim D. Brucker f908c4954b Enabled index generation. 2019-08-02 17:16:13 +01:00
Achim D. Brucker e09556133d Reworked figure for horizontal layout. 2019-08-02 16:43:28 +01:00
Achim D. Brucker fcb3f1e947 Removed files created and only readable by proprietary. 2019-08-02 16:43:03 +01:00
Achim D. Brucker 95dc57891b Ensured that DOF is already introduced in the introduction. 2019-08-02 16:24:37 +01:00
Achim D. Brucker 5668e3c56d Cleanup. 2019-08-02 12:19:00 +01:00
Achim D. Brucker 5e77466b39 Spell checking. 2019-08-02 12:04:41 +01:00
Achim D. Brucker 90add40145 Added citation information. 2019-08-02 11:54:02 +01:00
Achim D. Brucker 390defe5e8 Highlight default prompt in shell sessions. 2019-08-02 11:12:38 +01:00
Achim D. Brucker 13a6384cfe Updated introduction and started content restructuring. 2019-08-02 11:12:16 +01:00
Achim D. Brucker 7c6a214e98 Added running headers. 2019-08-01 20:50:48 +01:00
Achim D. Brucker 423ea01309 Highlight antiquotations in (S)ML code. 2019-08-01 20:47:49 +01:00
Achim D. Brucker 3aa6fb00af Complete rewrite using tcolorbox. 2019-08-01 20:37:54 +01:00
Achim D. Brucker cafebd2846 Renamed lstisadof style, as it is now specific to the manual. 2019-07-31 13:26:01 +01:00
Achim D. Brucker 42faa428eb Added markers to listings environment and moved all listings configuration into lstisadof.sty. 2019-07-31 12:12:41 +01:00
Achim D. Brucker 3eba90f978 Revised abstract. 2019-07-30 22:57:22 +01:00
Achim D. Brucker c4671d3802 Improved reference to repository URL. 2019-07-29 07:21:39 +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. 2019-07-28 12:01:58 +01:00
Achim D. Brucker 458f076473 Fixed lstisar syntax. 2019-07-28 11:53:39 +01:00
Achim D. Brucker 8a2cfc1044 Improved title page. 2019-07-28 10:55:39 +01:00
Achim D. Brucker 75e04b164a Improved copyright informaton. 2019-07-26 16:13:20 +01:00
Achim D. Brucker d0306e62bc Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF 2019-07-23 15:31:03 +01:00
Achim D. Brucker 92e9dfb70f Swichted to document template scrreprt-modern. 2019-07-23 15:30:56 +01:00
Achim D. Brucker 6515237158 Various layout improvements. 2019-07-23 15:30:26 +01:00
Burkhart Wolff 6526fd2e70 04_RefMan.thy 2019-07-23 16:04:08 +02:00
Burkhart Wolff b894ee31a0 Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF 2019-07-23 15:27:03 +02:00
Burkhart Wolff 97701d62d7 local improvements due to remarks of Frederic. 2019-07-23 15:26:48 +02:00
Achim D. Brucker 2a65c04ac6 Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF 2019-07-23 12:17:04 +01:00
Burkhart Wolff bf4255dbf9 Many little things 2019-07-23 09:41:15 +02:00
Burkhart Wolff 68f865557b corrected affiliation 2019-07-23 08:56:51 +02:00
Achim D. Brucker 78dbffe763 Updated title. 2019-07-23 07:51:27 +01:00
Burkhart Wolff f583ea60c3 Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF 2019-07-22 16:36:00 +02:00
Burkhart Wolff 502c1460b4 restructuring of section 4, some polishing intro. 2019-07-22 16:35:57 +02:00
Achim D. Brucker c5413107af Added Isabelle/DOF logo. 2019-07-22 15:07:59 +01:00
Achim D. Brucker a644634cf9 Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF 2019-07-22 14:41:53 +01:00
Achim D. Brucker 281cb5541c Fixed naming inconsistency. 2019-07-22 14:41:29 +01:00
Burkhart Wolff 856f652082 added sections on conservative term programming and a definition example as specification construct 2019-07-22 15:37:47 +02:00
Achim D. Brucker ecbb18fac8 Added license information. 2019-07-21 16:47:33 +01:00
Achim D. Brucker f734c0eb5e Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF 2019-07-21 16:15:02 +01:00
Achim D. Brucker 6f574e49d5 Updated author information. 2019-07-21 16:14:42 +01:00
Achim D. Brucker c5a6d686c8 Removed availability information. 2019-07-21 16:14:32 +01:00
Achim D. Brucker 432d2f0ba3 Updated listings setup. 2019-07-21 16:02:46 +01:00
Burkhart Wolff 36ff213103 more experiments 2019-07-21 16:35:08 +02:00
Burkhart Wolff f3c5aed97a more experiments 2019-07-21 16:26:33 +02:00