Burkhart Wolff
f9027ef331
a section explaining the consequences of a doc-class and its shallow semantics in Isabelle records on different levels of representation
2021-07-18 17:34:52 +02:00
Achim D. Brucker
6c433ed766
Merge pull request 'class-term-antiquotation-implementation' ( #2 ) from nicolas.meric/Isabelle_DOF:class-term-antiquotation-implementation into master
...
Reviewed-on: Isabelle_DOF/Isabelle_DOF#2
2021-07-02 17:39:52 +02:00
Achim D. Brucker
cfbc3311cd
Merge branch 'master' into class-term-antiquotation-implementation
2021-07-02 17:39:42 +02:00
Achim D. Brucker
295233cdcf
Merge pull request 'all changes' ( #1 ) from nicolas.meric/Isabelle_DOF:eclectic-tutorial-add-todos-fix-typos into master
...
Reviewed-on: Isabelle_DOF/Isabelle_DOF#1
2021-07-02 17:33:32 +02:00
Achim D. Brucker
9569113f9b
Merge branch 'master' into eclectic-tutorial-add-todos-fix-typos
2021-07-02 17:27:26 +02:00
Burkhart Wolff
9f9bc25618
no message
2021-07-01 16:25:31 +02:00
Burkhart Wolff
5aad659a85
some observations on invariant code generation
2021-07-01 13:12:18 +02:00
Nicolas Méric
2c01a7118b
Add term* cmd and term antiquotations for classes
...
- Add a term antiquotation for document classes
and add the term* command which mimics the classical term command
and adds the possibility to use a term antiquotation
which references document classes:
one can use @{A ''A_instance''} to reference
an instance of the class A in a term* command.
- Reuse and update the ML_isa_check_generic visitor pattern
to add the function which checks the class instance of a class,
used by the term antiquotation for document classes.
Also, the update_isa functions now expect long name
(See builtin term antiquotations setup)
- The merge of ISA_transformer_tab has been update to avoid conflicts.
Indeed, the merge is ultra-critical: the transformer tabs were
just extended by letting *the first* entry
with the same long-name win.
Since the range is a (call-back) function, a comparison on its content
is impossible and some choice has to be made.
An alternative may be to use Symtab.join
- As classes names as constants are already bound to
"doc_class Regular_Exp.rexp" constants by add_doc_class_cmd function,
we use a prefix "doc_class_" when adding
document classes term antiquotations
2021-06-01 17:32:45 +02:00
Nicolas Méric
f11e5b762b
all changes
2021-06-01 14:51:22 +02:00
Burkhart Wolff
f8801a1121
basically table_inline.
2021-05-13 14:37:27 +02:00
Burkhart Wolff
d7b625ae04
little debug.
2021-04-21 20:27:23 +02:00
Burkhart Wolff
3b21df199b
addded docitem ML antiquotation. (Kleine Fingeruebung).
2021-04-21 20:24:06 +02:00
Achim D. Brucker
0b6ef076b0
Initial support for svjour3-class from Springer.
2021-04-06 12:15:13 +01:00
Achim D. Brucker
51375ea983
Updated TeX Live dependency to version 2021.
2021-04-01 23:47:35 +01:00
Achim D. Brucker
78987a5ae0
Fixed MarkDown.
2021-03-22 00:40:59 +00:00
Achim D. Brucker
920779b150
Raised requirement of Tex Live to TeX Live 2021 (expected release date: 4th of April 2021).
2021-03-22 00:13:18 +00:00
Achim D. Brucker
e20e73be90
Added ERT 2018 publication and added note about required version of tcolorbox.sty.
2021-03-22 00:12:00 +00:00
Achim D. Brucker
b96397800d
Updated Isabelle base image.
2021-03-21 00:00:13 +00:00
Achim D. Brucker
8d8d418f0e
Update after Isabelle/DOF 1.1.0/Isabelle2021 release.
2021-03-20 23:56:46 +00:00
Achim D. Brucker
712cea7ac9
Merge branch 'v1.1.x/Isabelle2020'
2021-03-20 22:26:14 +00:00
Achim D. Brucker
0300a64119
Added v.1.1.0.
2021-03-20 22:25:29 +00:00
Achim D. Brucker
6d166ecee4
Added links for 1.1.0/Isabelle2020 release.
2021-03-20 22:19:57 +00:00
Achim D. Brucker
a0654d8db9
Added Nicolas Méric as contributor.
2021-03-20 22:05:57 +00:00
Achim D. Brucker
e048bbe508
Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
2021-03-15 10:25:16 +00:00
Achim D. Brucker
201d12a01a
Fixed spelling.
2021-03-15 10:24:58 +00:00
Achim D. Brucker
aadbce7844
Removed direct link to TeX Live installation instructions that are somewhat misleading for OS X users. The main TeX Live instructions are, actually, more helpful.
2021-03-15 10:24:31 +00:00
Burkhart Wolff
cfad21e296
Ref auf Makarius Text added
2021-03-14 15:45:42 +01:00
Burkhart Wolff
ad18d3c179
...
2021-03-14 12:03:52 +01:00
Achim D. Brucker
46875b0560
Fixed version number.
2021-03-11 00:03:37 +00:00
Achim D. Brucker
389fd6d033
Switch from pdf(la)tex to lua(la)tex.
2021-03-10 23:51:18 +00:00
Achim D. Brucker
f975672901
Removed check for \expanded{}: Isabelle 2021 defaults to luatex as TeX-engine, which has \expanded{} since a very long time.
2021-03-10 22:12:39 +00:00
Achim D. Brucker
4a1f15be02
Removed check for \expanded{}: Isabelle 2021 defaults to luatex as TeX-engine, which has \expanded{} since a very long time.
2021-03-10 22:10:12 +00:00
Achim D. Brucker
06dddeacf5
Porting to Isabelle 2021.
2021-03-10 22:04:09 +00:00
Achim D. Brucker
e495a7b2fe
Revising Chapter 5.
2021-02-13 17:04:17 +00:00
Achim D. Brucker
018bfa4bcd
Added default escapechar for ltx environment.
2021-02-12 02:24:31 +00:00
Achim D. Brucker
15c958ec64
Revised Chapter 4.
2021-02-11 19:10:38 +00:00
Achim D. Brucker
29661f6734
Revised Sec. 4.2.
2021-02-10 09:05:59 +00:00
Achim D. Brucker
3649fb855e
Revised Sec. 4.1.
2021-02-09 20:56:56 +00:00
Achim D. Brucker
43184a9995
Migrated \inlinebawsh{}.
2021-02-08 15:34:59 +00:00
Achim D. Brucker
ed8cd2ad9d
Migrated \inlinebawsh{}.
2021-02-08 15:33:45 +00:00
Achim D. Brucker
029ae709e6
Migrated \inlineltx{}, except when argument contained { or }.
2021-02-07 20:01:43 +00:00
Achim D. Brucker
85d94848b6
Revised Chapter 3.
2021-02-06 12:08:18 +00:00
Achim D. Brucker
b61346fd64
Revised Sec. 3.2.
2021-02-05 06:58:22 +00:00
Achim D. Brucker
3d0cbf6a4f
Revised Sec. 3.1.
2021-02-04 18:52:38 +00:00
Achim D. Brucker
50d3dde1a0
Converted \inlinesml{...}.
2021-02-03 05:13:05 +00:00
Achim D. Brucker
d605e23218
Converted \inlinesml{...}.
2021-02-02 12:22:35 +00:00
Achim D. Brucker
2d3e521296
Converted \inlinebash{...}.
2021-02-02 12:20:03 +00:00
Achim D. Brucker
b81eef7bd2
Converted bash-environments to antiqotations.
2021-02-01 05:06:15 +00:00
Achim D. Brucker
a1332ec9a4
Converted bash-environments to antiqotations.
2021-01-31 16:54:22 +00:00
Achim D. Brucker
243556467a
Merge remote-tracking branch 'origin/add-todos-fix-typos'
2021-01-30 06:47:47 +00:00