Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity
1,593 Commits 14 Branches 9 Tags 76 MiB
Commit Graph

325 Commits

Author SHA1 Message Date
Nicolas Méric 35b50e419f Update related work and enable checking for section 5 
Also fix typos
 2022-04-20 14:51:39 +02:00
Nicolas Méric 9b396b6096 Merge branch 'main' into ICFEM-2022 2022-04-20 09:32:08 +02:00
Nicolas Méric d8fde4b4f4 Cleanup and add test for meta-args for assert*
ci/woodpecker/push/build Pipeline was successful Details
2022-04-19 14:05:52 +02:00
Burkhart Wolff c9beb99b7a Elements in the intro 
- enlarging the scope to engineering
- addig recfs.
 2022-04-19 14:02:37 +02:00
Achim D. Brucker 41e6c9ed02 Fixed file attributes.
ci/woodpecker/push/build Pipeline was successful Details
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 64b4eca5ea Avoid using natbib.
ci/woodpecker/push/build Pipeline failed Details
2022-04-15 21:56:01 +01:00
Achim D. Brucker 317c5a7759 Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
ci/woodpecker/push/build Pipeline failed Details
2022-04-15 21:03:59 +01:00
Achim D. Brucker 530783c23b Bug fix: handling of arguments for top-level author* command. 2022-04-15 20:49:05 +01:00
Burkhart Wolff 346b28f732 Added elements on Sec 5.
ci/woodpecker/push/build Pipeline was successful Details 
- storyline
- snippets of CENeLEC modeling.
 2022-04-13 17:19:29 +02:00
Burkhart Wolff de1354625e some elements in CENELEC.
ci/woodpecker/push/build Pipeline was successful Details 
- added roles to cenelec_document
- specified some invariants on them.
 2022-04-13 16:19:36 +02:00
Burkhart Wolff d0bedee42d syncing chap 4 with CENELEC
ci/woodpecker/push/build Pipeline was successful Details 
- shortend "knackified" example
- slight extensions of the CENELEC.
- layout improvements in CENELEC.
 2022-04-13 15:36:13 +02:00
Burkhart Wolff 76cff5beab some elements in sec 5
ci/woodpecker/push/build Pipeline was successful Details
2022-04-12 09:46:27 +02:00
Burkhart Wolff 6f4259cc2c added an Interface Element into cENeLEC
ci/woodpecker/push/build Pipeline was successful Details
2022-04-08 15:56:03 +02:00
Nicolas Méric e3caad804b Fix {Theorem, Lemma}_default_class theory attributes
ci/woodpecker/push/build Pipeline was successful Details 
Fix #11
 2022-04-08 12:17:24 +02:00
Nicolas Méric 74420a932f Clean up check_invariants
ci/woodpecker/push/build Pipeline was successful Details
2022-04-07 15:36:01 +02:00
Nicolas Méric 8e1702d2da Add IDE reporting for attributes in meta-argument list
ci/woodpecker/push/build Pipeline was successful Details
2022-04-07 15:33:24 +02:00
Burkhart Wolff 65e6240fa8 some elements on cenelec
ci/woodpecker/push/build Pipeline was successful Details
2022-04-06 17:41:06 +02:00
Burkhart Wolff 74ba9aa892 ... 2022-04-06 09:29:10 +02:00
Achim D. Brucker 609f09e919 Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
ci/woodpecker/push/build Pipeline was successful Details
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
Nicolas Méric b1f73e9235 Delete Isabelle marks file
ci/woodpecker/push/build Pipeline was successful Details
2022-04-01 11:54:49 +02:00
Nicolas Méric d95a5aa2a8 Merge branch 'main' into test-merge 2022-04-01 09:59:22 +02:00
Nicolas Méric 9603311a9a Fix DOF manual and tests to work with assert*
ci/woodpecker/push/build Pipeline was successful Details
2022-04-01 09:54:16 +02:00
Burkhart Wolff 2351e00be6 corrected and re-inserted Ecclectic Man into build
ci/woodpecker/push/build Pipeline failed Details
2022-03-31 15:55:01 +02:00
Burkhart Wolff d2e1d77b01 some corrections in the Eccectic RefMan
ci/woodpecker/push/build Pipeline failed Details
2022-03-31 13:49:46 +02:00
Burkhart Wolff a68ecb4f11 ... 2022-03-31 10:12:46 +02:00
Burkhart Wolff 6a7b5c6afb fixed term* bug (non-evaluation of meta-args). Needs cleanup.
ci/woodpecker/push/build Pipeline failed Details
2022-03-31 06:57:18 +02:00
Burkhart Wolff 9403afd86f addressing the value* transmission problem - not yet solved completely
ci/woodpecker/push/build Pipeline failed Details
2022-03-30 17:54:02 +02:00
Nicolas Méric e4e4a708a5 Update assert* to use isabelle/DOF evaluation
ci/woodpecker/pr/build Pipeline failed Details
2022-03-30 08:12:17 +02:00
Nicolas Méric 444d6d077c Add eager and lazy elaboration 
- Isabelle uses eager evaluation, so should the elaboration of terms
  which are evaluated.
  The value of instances are now registered in the data tables
  of Isabelle/DOF when fully elaborated, ie,
  term annotation antiquotations proposed by Isabelle/DOF in
  an instance value are replaced by its value before registration
  in Isabelle/DOF data
  A new field, input_term, stores the lazy elaboration
  and is used when elaboration is not wished
  (to print the original input term declared by the user, for example)
- Clean up the simplication mechanism of the internal trace attribute
  (used by monitor classes)
 2022-03-29 15:22:44 +02:00
Nicolas Méric ec33e70bbf Loosen dependency on Toplevel.transition 
Loosen the dependency of the implementation of value* and term*
on Toplevel.transition.
Toplevel.transition should be avoided as it has specific behaviors
like only allowing atomic transactions.
 2022-03-29 15:22:44 +02:00
Achim D. Brucker f655d2a784 Removed adding build script (no longer needed).
ci/woodpecker/push/build Pipeline was successful Details
2022-03-27 21:40:51 +01:00
Achim D. Brucker d80d5b0538 Support for local styles and templates.
ci/woodpecker/push/build Pipeline was successful Details
2022-03-27 21:29:25 +01:00
Achim D. Brucker 7b8ae0a93d Make use of install script optional in favor of registration as Isabelle component. Style files, templates, and scripts are no longer installed into ISABELLE_USER_HOME.
ci/woodpecker/push/build Pipeline was successful Details
2022-03-27 13:21:55 +01:00
Achim D. Brucker 700855411e Do not register build script in default ROOT file (no longer needed). 2022-03-27 12:21:14 +01:00
Achim D. Brucker 5348a609be Official support for lipics-v2021 (fixes #13). 2022-03-27 12:20:49 +01:00
Achim D. Brucker 46c46af880 Removed outdated lipics v2019 setup. 2022-03-27 12:02:48 +01:00
Achim D. Brucker 7b4450450d Hide use of build script from users. 2022-03-27 12:02:15 +01:00
Achim D. Brucker 1d48fb810f Updated messages to users and removed outdated checks. 2022-03-27 11:01:20 +01:00
Achim D. Brucker 05e85edd91 Removed non-distribution note for llncs.cls. This class is now available on CTAN and part of TeXLive (at least from version 2022).
ci/woodpecker/push/build Pipeline failed Details
2022-03-26 21:31:05 +00:00
Achim D. Brucker 846237b515 Support for Isabelle 2021-1. 2022-03-26 21:25:40 +00:00
Achim D. Brucker aff78b0625 Restructuring.
ci/woodpecker/push/build Pipeline failed Details
2022-03-26 19:31:23 +00:00
Achim D. Brucker 3c49a9aaba Removed outdated test session. 2022-03-26 18:53:33 +00:00
Achim D. Brucker ef89a95307 Fixed oversight during merge and removed patches that are no longer needed. 2022-03-20 22:41:09 +00:00
Achim D. Brucker 62726920a7 Fixed oversight during merge and removed patches that are no longer needed. 2022-03-20 22:39:18 +00:00