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
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
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
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
Burkhart Wolff
5d7b50ca7f
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2023-04-27 13:03:07 +02:00
Burkhart Wolff
1ebfaccb50
amended explication of examples.
2023-04-27 13:02:57 +02:00
Achim D. Brucker
101f96a261
Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
2023-04-26 08:16:39 +01:00
Achim D. Brucker
49aa29ee68
Normalised LaTeX command names.
2023-04-26 08:16:32 +01:00
Burkhart Wolff
2919f5d2a5
animation over ontologies vs. meta-language
2023-04-26 07:14:46 +02:00
Burkhart Wolff
6cafcce536
boxed sml preserves now $.
2023-04-25 22:05:33 +02:00
Burkhart Wolff
ebce149d6a
...
2023-04-25 17:50:05 +02:00
Burkhart Wolff
6984b9ae03
minor stuff
2023-04-25 17:09:36 +02:00
Burkhart Wolff
74e2341971
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2023-04-25 16:21:05 +02:00
Burkhart Wolff
16caefc7be
revision/restructuring > pp 40
2023-04-25 16:20:58 +02:00
Burkhart Wolff
761a336a7a
Nicos improvements.
2023-04-24 12:05:04 +02:00
Burkhart Wolff
77aeb3b7ca
...
2023-04-20 14:29:38 +02:00
Burkhart Wolff
f093bfc961
...
2023-04-20 11:46:50 +02:00
Burkhart Wolff
2c7df482e8
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2023-04-20 09:47:30 +02:00
Burkhart Wolff
c9de5f2293
put ltxinline into macro notation
2023-04-20 09:47:22 +02:00
Nicolas Méric
c6dc848438
Some cleanup
2023-04-20 08:30:09 +02:00
Burkhart Wolff
1acf863845
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2023-04-19 21:50:51 +02:00
Burkhart Wolff
a6aca1407e
added sec on term atq, restructuring
2023-04-19 21:50:43 +02:00
Burkhart Wolff
4c953fb954
revised sec 3
2023-04-19 21:17:07 +02:00
Nicolas Méric
939715aba9
Fix scholarly_paper
2023-04-19 15:53:31 +02:00
Burkhart Wolff
d809211481
revision to 2 completed, still todo'ds in 3 and 4 and beyond
2023-04-19 13:17:26 +02:00
Achim D. Brucker
a5885b3eb5
Fixed ref/label setup.
2023-04-14 20:56:43 +01:00
Burkhart Wolff
3ab6f665eb
rearranging the story in Background
2023-04-13 22:00:35 +02:00
Burkhart Wolff
0c8bc2cab3
new high-level presentations in background
2023-04-13 18:29:10 +02:00