121 Commits

Author	SHA1	Message	Date
Nicolas Méric	7791538b54	Update to isabelle 2023 and add morphism examples	2024-04-04 12:08:25 +02:00
Nicolas Méric	10b98b660f	Fix typo	2024-03-12 16:02:25 +01:00
Nicolas Méric	a1677384b3	Update bug declare_reference* bug example	2024-03-11 15:51:34 +01:00
Nicolas Méric	46b094939a	Update bug example in Test_Polymorphic_Classes	2024-03-04 14:32:46 +01:00
Nicolas Méric	42da18cf3a	Reference a bug in polymorphic class implementation	2024-03-04 14:30:58 +01:00
Nicolas Méric	207029e70e	Enable term anti-quotations in class invariants	2024-02-14 11:15:13 +01:00
Nicolas Méric	7b54bf5ca5	Cleanup	2023-09-20 15:56:50 +02: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	4393042f2c	Merge.	2023-08-29 08:09:28 +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	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
Nicolas Méric	5a07aa2453	Delete useless tests	2023-06-16 18:37:00 +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	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
Achim D. Brucker	c803474950	Merge branch 'main' into isabelle_nightly	2023-05-19 16:19:00 +02:00
Nicolas Méric	4d89250606	Restrict RegExpInterface notations to onto class definition	2023-05-16 12:27:19 +02:00
Achim D. Brucker	3f06320034	Merge branch 'main' into isabelle_nightly	2023-05-15 17:56:39 +02:00
Achim D. Brucker	49faed4faf	Disabled PDF generation for currently not supported references.	2023-05-15 17:55:52 +02:00
Achim D. Brucker	1a22441f3e	Merge branch 'main' into isabelle_nightly	2023-05-15 14:31:01 +02:00
Burkhart Wolff	bce097b1d6	Commenting out refs to definitionSTAR	2023-05-15 13:02:41 +02:00
Achim D. Brucker	4adbe4ce81	Merge branch 'main' into isabelle_nightly	2023-05-15 10:20:12 +02:00
Nicolas Méric	cd311d8a3a	Update firgure* implementation	2023-05-15 09:36:02 +02:00
Burkhart Wolff	db4290428f	...	2023-05-13 18:22:27 +02:00
Burkhart Wolff	43da6d3197	...	2023-05-13 18:20:29 +02:00
Achim D. Brucker	a93046beac	Merge.	2023-05-13 00:09:44 +02:00
Burkhart Wolff	e97cca1a2c	reactivated Cenelec_Test	2023-05-12 17:17:57 +02:00
Burkhart Wolff	33fd1453a0	Global remove of side-by-side-figures, fixing various bugs - Caveat: no correspondance figure* - class figure.	2023-05-12 17:04:30 +02:00
Burkhart Wolff	543c647bcc	Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF	2023-05-12 16:19:29 +02:00
Burkhart Wolff	f7141f0df8	debugging the LaTeX generation for COL	2023-05-12 16:19:14 +02:00
Burkhart Wolff	514ebee17c	pass on new figure implemntation	2023-05-12 15:11:37 +02:00
Nicolas Méric	7e01b7de97	Implement long names for classes term-antiquotataions ... Examples with value* that now work: value*‹@{scholarly-paper.author ‹church'›}› value*‹@{author ‹church›}› value*‹@{Concept-High-Level-Invariants.author ‹church›}› value*‹@{scholarly-paper.author-instances}› value*‹@{author-instances}› value*‹@{Concept-High-Level-Invariants.author-instances}›	2023-05-11 19:02:55 +02:00
Burkhart Wolff	8bdd40fc20	basic problems on multiple subfloats content solved	2023-05-11 16:21:37 +02:00
Burkhart Wolff	36740bf72b	debugging fig_content	2023-05-11 11:48:05 +02:00
Burkhart Wolff	b8da1a304a	Improved fig_content, fix backend bugs in COL_Test	2023-05-10 18:31:27 +02:00
Burkhart Wolff	50da7670cf	Some repair on the coherence problems in COL	2023-05-10 15:54:02 +02:00
Burkhart Wolff	0aa9f1ff25	renamed figure2 into float	2023-05-10 12:37:29 +02:00
Burkhart Wolff	ca8671ee1c	a version with @{fig_content in the test	2023-05-09 23:12:50 +02:00
Burkhart Wolff	9e210b487a	a version with @{fig_content in the test	2023-05-09 23:08:57 +02:00
Burkhart Wolff	322d70ef69	deleting subparagraph (never used),orienting Example-I on figure2.	2023-05-09 16:15:47 +02:00
Burkhart Wolff	b04ff7e31a	Some first test on the COL library, assuring coherence between text* and figure* versiona.	2023-05-09 12:59:42 +02:00
Achim D. Brucker	47e8fc805f	Merge branch 'main' into Isabelle_dev	2023-04-27 14:54:52 +01:00
Nicolas Méric	93c722a41b	Update malformed theory names ... Theory names should use Isabelle inner syntax to allow objects referencing using long names. For inner syntax, see the isar-ref manual about syntax category "longid", which is the same as "long_ident" of outer syntax (but not "name" or "system_name").	2023-04-27 14:53:17 +02:00
Achim D. Brucker	0d74645d2e	Merge and upgrade to development version of Isabelle/HOL.	2023-04-24 22:26:39 +01:00