Burkhart Wolff
013296f25e
experiments on tables
2022-06-26 13:48:03 +02:00
Burkhart Wolff
c16ec333f1
experiments on multi-commands - multi-figures
2022-06-24 08:15:03 +02:00
Burkhart Wolff
d1e4fd173b
Experiments with multi-commands and -figures.
...
- added multi-arg syntax (only one arg evaluated so far)
- added figure_content built-in antiquotation
- added new Figure* - multi-arg command.
2022-06-22 16:32:31 +02:00
Burkhart Wolff
43c857af2c
roughly ported Latex testbench to 21-1
2022-06-17 20:35:32 +02:00
Burkhart Wolff
0cc010cecc
debugged merge
2022-06-17 09:37:43 +02:00
Burkhart Wolff
ba7bd6dc03
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2022-06-17 09:31:29 +02:00
Burkhart Wolff
43b0a3049f
Modelling sample for tables
2022-06-17 09:31:17 +02:00
Nicolas Méric
03fd491d5d
Implement CENELEC Table A.1
...
- Add an eager and lazy invariants checking functions mechanism
for low level invariants to allow the checking of invariants
only when opening or closing a monitor instance.
The state of the monitor instances traces evolves when declaring
instances between open_monitor* and close_monitor* commands.
This mechanism can capture the changes be defining
invariants before or after traces are populated but not
before and after, with the current mechanism.
Two tables were added: docclass_eager_inv_tab
and docclass_lazy_inv_tab to store these invariants
- Implement CENELEC_50128 Table A.1 using this mechanism
2022-06-13 07:56:53 +02:00
Nicolas Méric
9673359688
Enable high level invariants checking for some commands
...
Enable high level invariants checking for the update_instance*
and close_monitor* commands
2022-05-27 17:14:17 +02:00
Nicolas Méric
5d1b271336
Allow access to the monitor table for low level invariants
...
When defining low level invariants checking functions,
access to the monitor table might be useful.
So the table should be populated before the checking takes place.
2022-05-27 14:46:04 +02:00
Nicolas Méric
83c790d66a
Handle normalization of trace attribute
2022-05-26 12:56:21 +02:00
Nicolas Méric
9981c31966
Normalize docobj table value
...
Normalize the record registered as value in the docobj table,
i.e., the logical value of a docitem (a class instance)
2022-05-25 17:10:57 +02:00
Nicolas Méric
319b39905f
Update CENELEC_50128 implementation
...
- Update phase datatype to be accurate with 7.3 in the standard
- Update cenelec_document class: according to the table C.1 in the
standard, written by, first check, and second check can be optional.
See Phase Planning line 4 in the table, for example
- Some specifications are external to the standard: implement them
as external_specification subclasses
- Fix phases attributes of classes
2022-05-18 18:23:57 +02:00
Nicolas Méric
c00c6ed31d
Fix Terms and Definitons section in CENELEC
2022-05-12 16:04:09 +02:00
Nicolas Méric
ae3300ac2c
Import of CENELEC_50128.thy changes from /ICFEM-2022
2022-05-11 18:15:33 +02:00
Achim D. Brucker
61f167c29c
Made all import paths globally qualified.
2022-05-06 09:17:10 +01:00
Achim D. Brucker
2833deff90
Harmonizing the various root templates.
2022-04-22 20:51:42 +01:00
Achim D. Brucker
a8424979eb
Removed support for oldstyle font commands.
2022-04-21 22:59:11 +01:00
Achim D. Brucker
15e71fe189
Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
2022-04-20 11:08:29 +01:00
Achim D. Brucker
45c23b4330
Fixed environment for isamarkupabstract.
2022-04-20 11:07:06 +01:00
Nicolas Méric
d8fde4b4f4
Cleanup and add test for meta-args for assert*
2022-04-19 14:05:52 +02:00
Achim D. Brucker
41e6c9ed02
Fixed file attributes.
2022-04-18 09:44:44 +01:00
Achim D. Brucker
cbad96aba5
Fixed file attributes.
2022-04-18 09:22:57 +01:00
Achim D. Brucker
82c9a07c1a
Fixed file attributes.
2022-04-18 09:20:55 +01:00
Achim D. Brucker
ae8b91ac4e
Fixed file attributes.
2022-04-18 09:20:36 +01:00
Achim D. Brucker
0f3f5d4b56
Fixed file attributes.
2022-04-17 16:32:12 +01:00
Achim D. Brucker
fee83a2a29
Remove outdated and obsoleted ontologies.
2022-04-16 09:13:31 +01:00
Achim D. Brucker
a0993b6eea
Initial commit.
2022-04-15 22:05:19 +01:00
Achim D. Brucker
64b4eca5ea
Avoid using natbib.
2022-04-15 21:56:01 +01:00
Achim D. Brucker
2e4fb5d174
Added development version of authorarchive.sty, as version in TexLive 2022 is outdated.
2022-04-15 21:13:10 +01:00
Achim D. Brucker
317c5a7759
Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
2022-04-15 21:03:59 +01:00
Achim D. Brucker
12f1b230e6
Use LNCS template.
2022-04-15 21:01:53 +01:00
Achim D. Brucker
530783c23b
Bug fix: handling of arguments for top-level author* command.
2022-04-15 20:49:05 +01:00
Nicolas Méric
1457c1cb85
Fix typo in upd_meta_args rail road in manual
2022-04-08 13:04:50 +02:00
Nicolas Méric
e3caad804b
Fix {Theorem, Lemma}_default_class theory attributes
...
Fix #11
2022-04-08 12:17:24 +02:00
Nicolas Méric
17df6a271b
Delete some TODOs, now done, in the manual
2022-04-08 12:06:28 +02:00
Nicolas Méric
a331b80095
Update images for meta arguments list attribute exploration
...
Fix #10
2022-04-08 11:33:41 +02:00
Nicolas Méric
74420a932f
Clean up check_invariants
2022-04-07 15:36:01 +02:00
Nicolas Méric
8e1702d2da
Add IDE reporting for attributes in meta-argument list
2022-04-07 15:33:24 +02:00
Achim D. Brucker
609f09e919
Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
2022-04-04 16:04:51 +01:00
Achim D. Brucker
0f5e5bf6f6
Bug fix: -o option not working (reporting an error claiming that ontologies could not be found).
2022-04-04 16:04:10 +01:00
Achim D. Brucker
5c886d49b4
Defined basic set of options.
2022-04-03 22:45:47 +01:00
Nicolas Méric
b1f73e9235
Delete Isabelle marks file
2022-04-01 11:54:49 +02:00
Nicolas Méric
9603311a9a
Fix DOF manual and tests to work with assert*
2022-04-01 09:54:16 +02:00
Burkhart Wolff
2351e00be6
corrected and re-inserted Ecclectic Man into build
2022-03-31 15:55:01 +02:00
Burkhart Wolff
3e99e9e013
more discrepancies in the EcclecticMan solved.
2022-03-31 15:42:18 +02:00
Burkhart Wolff
d2e1d77b01
some corrections in the Eccectic RefMan
2022-03-31 13:49:46 +02:00
Burkhart Wolff
96726fc507
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2022-03-31 10:12:51 +02:00
Burkhart Wolff
a68ecb4f11
...
2022-03-31 10:12:46 +02:00
Achim D. Brucker
1ea897e660
Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
2022-03-31 06:39:46 +01:00