2072 Commits

All Branches

Search

Author	SHA1	Message	Date
Nicolas Méric	d59dabaf7c	Cleanup	2024-02-06 11:01:16 +01:00
Nicolas Méric	e78a114879	Fix typo	2023-11-27 12:01:52 +01:00
Burkhart Wolff	443d63f3b5	Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF	2023-11-25 17:06:39 +01:00
Nicolas Méric	331fcd07f0	Update invariants checking ... Make invariants checking compatible with namespaces and the new invariants implementation	2023-11-20 16:57:01 +01:00
Nicolas Méric	5dc20889a8	Partially implement polymorphic classes support for class invariants	2023-11-08 08:47:54 +01:00
Burkhart Wolff	e2b3184a77	Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF	2023-09-21 04:58:34 +02:00
Nicolas Méric	7b54bf5ca5	Cleanup	2023-09-20 15:56:50 +02:00
Nicolas Méric	baa36b10c1	Cleanup	2023-09-20 15:00:43 +02:00
Nicolas Méric	c57ce6292b	Update output type name for latex refs	2023-09-19 17:03:00 +02:00
Achim D. Brucker	b698572146	Documented Isabelle version (2023).	2023-09-14 06:33:28 +01:00
Achim D. Brucker	e12abadc94	Test with Isabelle 2023.	2023-09-14 06:29:01 +01:00
Achim D. Brucker	792fd60055	Merge branch 'main' into isabelle_nightly	2023-09-12 18:58:58 +01:00
Nicolas Méric	ec7297f1d3	Update instances list term antiquotation ... Make instances list term antiquotation compatible with polymorphic classes	2023-09-11 09:07:10 +02:00
Achim D. Brucker	e4ee3ff240	Merge branch 'main' into isabelle_nightly	2023-08-31 08:27:53 +01:00
Achim D. Brucker	4393042f2c	Merge.	2023-08-29 08:09:28 +01:00
Achim D. Brucker	fef7b9d60b	Merge commit 'cef4086029' into isabelle_nightly	2023-08-29 06:40:37 +01:00
Achim D. Brucker	ab7d695a77	Merge.	2023-08-29 06:37:33 +01:00
Achim D. Brucker	c063287947	Isabelle API update.	2023-08-29 06:11:32 +01:00
Achim D. Brucker	342984df3b	Converted def into newcommand.	2023-08-04 07:01:42 +01:00
Achim D. Brucker	5a8e79fb7e	Moved default value for title into template, as some LaTeX classes do not allow for a pre-set title.	2023-08-04 04:37:14 +01:00
Achim D. Brucker	d7f9f10ef1	Merge commit 'b4f1b8c32177ce5af37357fc4a7ab0df22a497d6' into isabelle_nightly	2023-08-03 03:41:43 +01:00
Achim D. Brucker	0a3259fbca	Merge commit '59b082d09d55d55ef6c6f8bd8e821122dddf3574' into isabelle_nightly	2023-08-03 03:35:29 +01:00
Nicolas Méric	ca7cdec9b4	Fix typos	2023-07-20 16:31:08 +02:00
Nicolas Méric	43aad517b9	Add basic explanation for lemma*, etc. ... Add basic explanation how to use lemma*, etc. with term antiquotations of polymorphic class instances	2023-07-20 16:25:25 +02:00
Nicolas Méric	8d6c8929e2	Fix typos	2023-07-20 16:14:25 +02:00
Nicolas Méric	b447a480fb	Fix manual latex compilation	2023-07-20 15:04:39 +02:00
Nicolas Méric	a78397693e	Update instances term antiquotation in manual	2023-07-20 14:32:03 +02:00
Nicolas Méric	9812bc0517	Use binding for instances name	2023-07-20 10:11:48 +02:00
Nicolas Méric	b364880bfc	Polymorphic classes first draft	2023-07-19 18:58:04 +02:00
Burkhart Wolff	d835665b6b	Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF	2023-07-19 12:54:57 +02:00
Burkhart Wolff	1a8cdb8014	...	2023-07-19 12:48:42 +02:00
Nicolas Méric	5a7cbf2da5	Add file checking in figure_content	2023-06-20 11:05:11 +02:00
Nicolas Méric	7f7780f8fd	Update restriction of RegExpInterface notations to onto class definition	2023-06-19 19:10:21 +02:00
Nicolas Méric	889805cccc	Add basic block environment support for beamer	2023-06-19 09:19:28 +02:00
Nicolas Méric	5a07aa2453	Delete useless tests	2023-06-16 18:37:00 +02:00
Nicolas Méric	cef4086029	Add basic support for beamer frame options and add a figure_content antiquotation	2023-06-16 11:54:33 +02:00
Nicolas Méric	9df276ac6f	Add first beamer frame implementation in SML	2023-06-15 16:07:08 +02:00
Nicolas Méric	b4f1b8c321	Fix ECs latex list of tables	2023-06-06 19:03:20 +02:00
Nicolas Méric	59b082d09d	Handle "_" and "'" in mixfix to be compatible with inner syntax names	2023-06-06 16:44:11 +02:00
Achim D. Brucker	1869a96b2d	API update.	2023-06-04 12:01:38 +02:00
Achim D. Brucker	e95c6386af	Merge branch 'main' into isabelle_nightly	2023-06-04 10:20:13 +02:00
Achim D. Brucker	23a85cc8c2	Minor tuning of beamer-related examples.	2023-06-01 17:58:55 +02:00
Achim D. Brucker	ddcfb5f708	Initial commit: stubs for using beamer.	2023-06-01 00:21:19 +02:00
Achim D. Brucker	02d13cdcad	Fixed release script.	2023-05-27 21:48:04 +02:00
Achim D. Brucker	d353ff07cc	Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF	2023-05-27 20:56:56 +02:00
Achim D. Brucker	38035785da	Fixed SRAC definition.	2023-05-27 20:56:47 +02:00
Achim D. Brucker	7e7c197ac3	Merge branch 'main' into isabelle_nightly	2023-05-25 11:42:31 +02:00
Nicolas Méric	4f8e588138	Document disable_assert_evaluation theory atttribute in the manual	2023-05-24 14:17:16 +02:00
Nicolas Méric	2c0b51779e	Add the possibility to disable evaluation for assert*	2023-05-24 12:38:29 +02:00
Nicolas Méric	350ff6fe76	Make class invariants long-names unique ... Now class invariants names use internally the class name as a user Binding.qualifier. This way one can use the same name for an invariant in two different classes in the same theory: doc_class "hypothesis" = math_content + referentiable :: bool <= "True" level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "hypt" invariant d :: "mcc σ = hypt" doc_class "math_proof" = math_content + referentiable :: bool <= "True" level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "prf_stmt" invariant d :: "mcc σ = prf_stmt" find_consts name:"math_proof.d_inv" find_consts name:"hypothesis.d_inv"	2023-05-23 14:44:16 +02:00