448 Commits

Author	SHA1	Message	Date
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.	2019-10-01 17:57:26 +02:00
Achim D. Brucker	b863a0178f	Define new TOCs only when used together with the KOMA-Script classes.	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.	2019-08-18 14:05:00 +01:00
Achim D. Brucker	39919ad3e1	Fixed typo.	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.	2019-08-17 16:31:27 +01:00
Achim D. Brucker	a30bf33d99	Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF	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.	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.	2019-08-17 09:40:25 +01: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	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	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.	2019-08-13 09:46:20 +01:00
Achim D. Brucker	b1d4abbf48	Introduced \dofurl.	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.	2019-08-04 22:54:46 +01:00
Achim D. Brucker	6e6c4a81cb	Updated Isabelle/DOF repository URL.	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.	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.	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.	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.	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.	2019-07-27 09:39:40 +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	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.	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).	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