nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
1,954 Commits 32 Branches 0 Tags 62 MiB
Commit Graph

153 Commits

Author SHA1 Message Date
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
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 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 59b082d09d Handle "_" and "'" in mixfix to be compatible with inner syntax names 2023-06-06 16:44:11 +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
Achim D. Brucker e17f09e624 Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF 2023-05-19 16:16:30 +02:00
Achim D. Brucker 8051d4233e Ensure compatibility with TeX Live 2019 (as used by AFP's build servers). 2023-05-17 13:57:35 +02:00
Achim D. Brucker 2dc16b263f Removed root.tex (bug). 2023-05-17 12:19:30 +02:00
Achim D. Brucker c7debc577b Moved src formats into subfolder and removed them from ROOT file. 2023-05-17 09:16:41 +02:00
Achim D. Brucker 9c94593f45 Removed unused files. 2023-05-17 06:39:44 +02:00
Nicolas Méric 4d89250606 Restrict RegExpInterface notations to onto class definition 2023-05-16 12:27:19 +02:00
Nicolas Méric ba7c0711a8 Update documentation and some refactoring 2023-05-15 10:48:40 +02:00
Achim D. Brucker 7e698a9e69 Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF 2023-05-15 10:16:34 +02:00
Achim D. Brucker 2569db05c3 Pushed raggedbottom into templates. 2023-05-15 10:16:31 +02:00
Nicolas Méric cd311d8a3a Update firgure* implementation 2023-05-15 09:36:02 +02:00
Achim D. Brucker 1986d0bcbd Merge branch 'main' into idir-remarks 2023-05-15 06:34:34 +00:00
Achim D. Brucker bbac65e233 Proof reading. 2023-05-15 08:30:33 +02:00
Achim D. Brucker 641bea4a58 Improved documentation and fixed width-bug of figure* macro. 2023-05-15 00:01:30 +02:00
Burkhart Wolff d0cd28a45c eliminated side_by_side figure, actualized refman. 2023-05-14 17:35:00 +02:00
Nicolas Méric b8282b771e Cleanup 2023-05-12 20:04:44 +02:00
Achim D. Brucker 6bab138af6 Removed default author. 2023-05-12 17:50:17 +02:00
Achim D. Brucker fcc25f7450 Removed implementation of figure* and side_by_side_figure. 2023-05-12 17:47:18 +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
Burkhart Wolff bdc8477f38 Code Cleanup 2023-05-12 09:42:52 +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
Idir Ait-Sadoune 9cc03c0816 Idir remarks for the intrduction of the manual. 2023-05-11 13:18:12 +02:00
Idir Ait-Sadoune e9cfcdbcbc Idir remarks for the abstract of the manual. 2023-05-11 12:48:49 +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 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
Burkhart Wolff 713a24615f LaTeX sty Bug xrt figure2 2023-05-09 12:13:23 +02:00
Burkhart Wolff 7ffdcbc569 experiment with figure2 2023-05-09 04:14:57 +02:00
Nicolas Méric 18be1ba5f5 Clean up dead code 2023-04-27 15:16:47 +02: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
Nicolas Méric 0f48f356df Fix sml latex environment issue with "$" 2023-04-27 14:53:17 +02:00