709 Commits

Author	SHA1	Message	Date
Burkhart Wolff	fbefa85586	First steps to reform cicm paper	2020-11-04 03:27:24 +01:00
Burkhart Wolff	c991e693dc	tested and enforced new author* and abstract* macros.	2020-11-04 02:52:55 +01:00
Achim D. Brucker	0b52e5872d	Use author*.	2020-11-03 21:50:19 +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	1f403a09f6	dfg	2020-11-02 14:14:52 +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
Burkhart Wolff	f093b033f5	started pass on chap 4 in Refman.	2020-10-26 10:08:22 +01:00
Burkhart Wolff	3ba9454ac7	Slight improvements of the layout	2020-10-25 12:57:43 +01:00
Burkhart Wolff	3c6197e6ca	FINISHED MY PASS ON THE PROGRAMMING MANUAL.	2020-10-25 12:02:44 +01:00
Burkhart Wolff	7999ee9a38	recvision till line 2000 (Term Parsing)	2020-10-21 13:49:01 +02:00
Burkhart Wolff	9b2c08183e	recvision till line 2000 (Term Parsing)	2020-10-20 18:26:20 +02:00
Burkhart Wolff	9ad51e9d70	Actualized Para on Toplevel Management	2020-10-20 14:22:53 +02:00
Achim D. Brucker	538292b972	Fixed LaTeX compiliation error.	2020-10-06 04:45:30 +01:00
Burkhart Wolff	c554b12be2	minor embellishments	2020-09-29 10:15:12 +02:00
Burkhart Wolff	873eda8ee0	stiluebungen	2020-09-25 13:38:34 +02:00
Burkhart Wolff	cdc1e0a7d8	stiluebungen < 1150	2020-09-23 13:57:32 +02:00
Burkhart Wolff	2cdf9f3124	stiluebungen < 1150	2020-09-23 13:23:20 +02:00
Burkhart Wolff	bea648530b	pushup.	2020-09-22 16:57:50 +02: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
Burkhart Wolff	c1d6694b7c	stiluebungen am PML	2020-09-22 14:50:57 +02:00
Burkhart Wolff	ad6ba9e302	stiluebungen am PML	2020-09-21 21:24:08 +02:00
Burkhart Wolff	6f36efae7f	stiluebungen am PML	2020-09-21 19:41:47 +02:00
Burkhart Wolff	b9de7663b6	added some paras in Guided Tour, corrected figure config Bug, exercice de style in MyCommentedIsa	2020-09-19 12:49:37 +02:00
Burkhart Wolff	6c6644ae0c	Updated MyCommentedIsabelle (a little; finished Guided Tour	2020-09-18 17:01:49 +02:00
Burkhart Wolff	5c22b80fb4	Nearly complete pass through chap 3	2020-09-16 14:24:39 +02:00
Achim D. Brucker	137262890e	Improved 'verbatim' output (removed generated %-signs).	2020-09-15 07:28:32 +01:00
Burkhart Wolff	41ac6006f8	rough pass through the guided tour.	2020-09-09 16:51:59 +02:00
Burkhart Wolff	2f95c56060	Version mit LaTeX Bizarrerie - verbatim _	2020-09-09 14:54:09 +02:00
Burkhart Wolff	2d2f4320e0	intermediate status with LaTeX pblsm	2020-09-09 13:17:22 +02:00
Achim D. Brucker	58617e87e6	Conversion: \isadof -> \<^isadof>.	2020-09-08 13:45:09 +01:00
Achim D. Brucker	640929ea71	Removed listings-based Isar setup.	2020-09-08 07:41:09 +01:00
Achim D. Brucker	37a71a613e	Ad hoc conversion: \inlineisar|...| -> @{boxed_theory_text ... }.	2020-09-08 07:30:14 +01:00
Achim D. Brucker	3dabf4fc82	Improvements: @{boxed_theory_text [display] ... }.	2020-09-08 06:51:36 +01:00
Achim D. Brucker	109802a76a	Ad hoc conversion: \begin{isar}...\end{isar} -> @{boxed_theory_text [display] ... }.	2020-09-08 06:18:01 +01:00
Achim D. Brucker	6c2ad62df2	Cleanup.	2020-09-08 00:11:22 +01:00
Achim D. Brucker	ee251a8000	Removed unused LaTeX definitions and style files.	2020-09-08 00:01:50 +01:00
Achim D. Brucker	7956a3009a	Initial commit: style for providing theorem-like default environments.	2020-09-07 23:56:43 +01:00
Achim D. Brucker	75719a933a	Added 2020-iFM-CSP example based on scrartcl.cls.	2020-09-07 23:35:43 +01:00
Achim D. Brucker	6b4bd6fea4	Removed boxed isar.	2020-09-07 23:19:41 +01:00
Burkhart Wolff	685f020b22	more content in Guided Tour.	2020-09-07 23:17:36 +01:00
Burkhart Wolff	39efc61686	some inpuit on Guided Tour	2020-09-07 23:17:36 +01:00
Burkhart Wolff	2321945dc4	sdf	2020-09-07 23:17:36 +01:00
Burkhart Wolff	fd532d985a	activated the new markup wherever possible. Started to revise chap 3.	2020-08-28 17:41:16 +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	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	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	f239b36b49	Reworked textually abstract, intro, background. Eliminate \emph	2020-08-25 09:17:36 +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)	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	33fd8a0f7b	startpunkt	2019-11-12 10:27:34 +01: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	23f68ce6c8	Improved layout.	2019-08-15 13:40:03 +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	f59bd7608a	Rescaling.	2019-08-05 21:42:56 +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	f57888284f	Minor changes for demonstrating document support for SRAC, EC, assumption, and hypthesis.	2019-07-27 19:05:45 +01:00
Achim D. Brucker	3649197e1f	Added index style.	2019-07-27 19:04:45 +01:00
Achim D. Brucker	75e04b164a	Improved copyright informaton.	2019-07-26 16:13:20 +01:00
Achim D. Brucker	beeb948c77	Inital commit of a major revision of this example.	2019-07-25 10:50:09 +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
Achim D. Brucker	36f7ebc4bf	Fixed naming inconsistency.	2019-07-23 07:41: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
Burkhart Wolff	869a1d6729	more experiments	2019-07-21 16:18:14 +02:00
Burkhart Wolff	b88031ec27	Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF	2019-07-21 16:07:01 +02:00
Burkhart Wolff	269623ab74	added experiment with cartouche syntax ...	2019-07-21 16:06:51 +02:00
Achim D. Brucker	19c8963abd	Updated lstisadof.sty.	2019-07-21 10:41:06 +01:00
Achim D. Brucker	eef387198a	Updated URL of Isabelle/DOF repository.	2019-07-21 10:22:06 +01:00
Achim D. Brucker	d1f55e7f30	Do not include checking instructions in PDF.	2019-07-21 10:21:37 +01:00
Achim D. Brucker	92f8fa5c25	Fixed naming inconsistency (cenelec vs. CENELEC_50128).	2019-07-20 22:39:06 +01:00
Achim D. Brucker	6fd22a071f	Resolved naming inconsistency (mathex_onto vs. math_exam).	2019-07-20 21:51:55 +01:00
Achim D. Brucker	8953f37629	Large directory restructuring. ... 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
Achim D. Brucker	f8013d90a2	Updated Isar notation.	2019-07-20 16:08:47 +01:00
Achim D. Brucker	e6cea1156c	Activated MathExam.	2019-07-20 15:30:13 +01:00
Achim D. Brucker	7f8ea1c115	Removed outdated BAC2017 example.	2019-07-20 15:15:04 +01:00
Achim D. Brucker	a85bcacd5b	Moved unit tests into tests directory and added test session.	2019-07-20 14:54:31 +01:00
Achim D. Brucker	189110dc0f	Cleanup.	2019-07-20 12:43:58 +01:00
Achim D. Brucker	3d01c5faf8	Cleanup.	2019-07-20 12:37:21 +01:00
Achim D. Brucker	4f911f3a23	Cleanup.	2019-07-20 12:02:05 +01:00
Achim D. Brucker	00651b385e	Cleanup.	2019-07-20 12:01:33 +01:00
Achim D. Brucker	38bd13d7d0	Cleanup.	2019-07-20 11:27:44 +01:00
Achim D. Brucker	a2d8ee9e6b	Merged the two theories for testing attribute related features.	2019-07-20 11:23:41 +01:00
Burkhart Wolff	00877b728e	regexps	2019-07-19 16:24:47 +02:00
Burkhart Wolff	e74df1be4d	doc_class syntax	2019-07-19 15:36:11 +02:00
Burkhart Wolff	44395aff2e	subsection on the HOL modeling context	2019-07-19 14:44:12 +02:00
Burkhart Wolff	6c1ed8af85	Introducing parts from SEFM, restructuring	2019-07-18 22:40:55 +02:00
Burkhart Wolff	c181c2851c	Added first somewhat realistic syntax on annotated text elements	2019-07-17 21:10:18 +02:00
Burkhart Wolff	1704c17776	New Structure discussed with adb, different shot in intro, ref to SEFM paper, first railroad dgm	2019-07-17 19:08:59 +02:00
Burkhart Wolff	a28ceb98eb	New LaTeX chapter introduced. Structuring proposal	2019-07-17 16:06:55 +02:00
Burkhart Wolff	62cf2264a2	new config of the document	2019-07-17 15:41:03 +02:00
Burkhart Wolff	67d6caf2ad	Reworked/Synced Background chapter with SEFM paper	2019-07-17 14:51:45 +02:00
Burkhart Wolff	5ff3217493	Internal Layout Polishing	2019-07-17 10:47:25 +02:00
Burkhart Wolff	869644e3b5	Proof Example	2019-07-17 10:24:41 +02:00
Burkhart Wolff	4c4194d468	Proof Example	2019-07-17 10:21:34 +02:00
Burkhart Wolff	4329bd2602	A little more explanations, more ontolgical control	2019-07-17 08:23:54 +02:00
Burkhart Wolff	58c31b59e8	completed first draft. Checks till page 47.	2019-07-16 19:33:24 +02:00
Burkhart Wolff	a7f6ab4fbd	Para on Antiquotation Registration	2019-07-16 16:40:40 +02:00
Burkhart Wolff	6f2dabbdd2	Markup section aufgeraeumt.	2019-07-15 17:56:13 +02:00
Burkhart Wolff	8acd482b96	Continued pass till pp 36.	2019-07-15 17:45:46 +02:00
Burkhart Wolff	e9a353919f	Renommage, reord of 2 snd TR report. Arrived at page 26	2019-07-15 17:14:11 +02:00
Burkhart Wolff	f2bb4f6e31	Modifications / evolutions for the second TR example. ... Arrived at page 34.	2019-07-15 17:12:10 +02:00