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

1541 Commits

Author SHA1 Message Date
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 f6f6f32b50 Merge branch 'main' into config_as_options 2022-04-20 11:09:01 +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
Achim D. Brucker 995feb6685 Fixed environment for isamarkupabstract. 2022-04-20 11:06:35 +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