pierre.derathe
/
Isabelle_DOF
Archived
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
1,625 Commits 15 Branches 8 Tags 73 MiB
Commit Graph

93 Commits

Author SHA1 Message Date
Nicolas Méric c0afe1105e Enable high-level invariants checking everywhere 
By default invariants checking generates warnings.
If invariants_strict_checking theory option is enabled,
the checking generates errors.

- Update 2018-cicm-isabelle_dof-applications/IsaDofApplications.thy
  and 2020-iFM-CSP/paper.thy to pass the checking of
  the low level invariant checking function "check"
  in scholarly_paper.thy,
  which checks that the instances in a sequence of the same class
  have a growing level.
  For a sequence:
  section*[intro::introduction]‹ Introduction ›
  text*[introtext::introduction, level = "Some 1"]‹...›

  introtext must have a level >= than intro.

- Bypass the checking of high-level invariants
  when the class default_cid = "text",
  the top (default) document class.
  We want the class default_cid to stay abstract
  and not have the capability to be defined with attribute,
  invariants, etc.
  Hence this bypass handles docitem without a class associated,
  for example when you just want a document element to be referenceable
  without using the burden of ontology classes.
  ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close>

  The functions get_doc_class_global and get_doc_class_local trigger
  an error when the class is "text" (default_cid),
  then the functions like check_invariants which use it will fail
  if the checking is enabled by default for all the theories.
 2022-12-20 16:31:09 +01:00
Makarius Wenzel 44cae2e631 More formal management of ontologies in Isabelle/ML/Isar with output via Isabelle/Scala exports 2022-12-04 00:09:29 +01:00
Makarius Wenzel 912d4bb49e Maintain document template in Isabelle/ML via Isar commands: 
result becomes export artifact, which is harvested by Isabelle/Scala build engine
 2022-12-02 20:05:15 +01:00
Makarius Wenzel a6ab1e101e Update Isabelle + AFP URLs 2022-12-01 11:55:51 +01:00
Achim D. Brucker 6c0d325673 Use full qualified name for templates. 2022-06-26 19:06:49 +01:00
Achim D. Brucker 70b2647e7c Using full-qualified names for ontologies in ROOT files. 2022-06-26 18:45:47 +01:00
Achim D. Brucker b83f7a8abb Updated manual. 2022-06-24 16:58:07 +01:00
Achim D. Brucker ef674b5ae2 Migrated, tested, and debugged new configuration setup. 2022-06-24 14:48:49 +01:00
Achim D. Brucker 41e6c9ed02 Fixed file attributes. 2022-04-18 09:44:44 +01:00
Achim D. Brucker a0993b6eea Initial commit. 2022-04-15 22:05:19 +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 12f1b230e6 Use LNCS template. 2022-04-15 21:01:53 +01:00
Achim D. Brucker 7b4450450d Hide use of build script from users. 2022-03-27 12:02:15 +01:00
Achim D. Brucker 2314b2191f Resolved merge conflict. 2022-03-20 20:49:46 +00:00
Achim D. Brucker 53eb93367c Cleanup. 2022-03-11 10:41:06 +00:00
Achim D. Brucker 6cf004637c Removed ITP paper draft - on own branch. 2022-03-11 07:24:54 +00:00
Burkhart Wolff 5631010371 added figures from IFM 19 paper 2022-01-14 15:31:15 +01:00
Burkhart Wolff 68e9f64156 added figures from talk 2022-01-13 16:24:07 +01:00
Burkhart Wolff 647f8e86cc Reorg / shoprtening chap 2. 2022-01-11 20:53:07 +01:00
Burkhart Wolff b5939bc9db added basckground chapter . First flush. 2022-01-08 22:22:22 +01:00
Burkhart Wolff 6889e08f33 initial setup of RAS paper 2022-01-02 17:05:15 +01:00
Burkhart Wolff ef7d8caefb added background chapter 2022-01-01 21:03:31 +01:00
Makarius Wenzel 4e4995bde5 Isabelle/Scala build.props with some pro-forma services 
(unusual package name prevents problems with Maven/IntelliJ).
 2021-12-19 16:50:21 +01:00
Burkhart Wolff 96d6bb8e00 intro proposal completed 2021-12-19 13:31:42 +01:00
Burkhart Wolff 77150aefe2 more on intro 2021-12-19 10:38:00 +01:00
Makarius Wenzel ec49f45966 Adaptations for Isabelle2021-1. 2021-12-18 23:06:51 +01:00
Burkhart Wolff 12d33fa457 more on intro ... 2021-12-17 15:44:47 +01:00
Burkhart Wolff 616ff85721 ... 2021-12-16 15:13:34 +01:00
Burkhart Wolff b0a2214c40 added refs 2021-12-16 15:07:02 +01:00
Burkhart Wolff cbd32874cf Abstract 2021-12-16 14:55:04 +01:00
Burkhart Wolff 3f09aca090 added paper frame, small things. 2021-12-16 13:49:44 +01:00
Achim D. Brucker 9e605d2e3c Removed fixme. 2021-01-15 00:46:29 +00:00
Achim D. Brucker 6927781d26 Merge. 2021-01-09 06:32:17 +00:00
Achim D. Brucker d2dcc71229 Removed explicit vspaces to clean up layout. 2021-01-04 06:32:56 +00:00
Burkhart Wolff aee1d33709 renaming ISA's; new shortcuts; more content in the RefMan. 2021-01-02 15:57:28 +01:00
Burkhart Wolff 6899c4059e improved macro syntax 2020-12-22 20:37:15 +01:00
Burkhart Wolff 5593c22a36 first version with macro syntax (no ML support) 2020-12-22 19:50:00 +01:00
Burkhart Wolff de5c0fc6e2 added Isar-syntax for define_shortcut* 2020-12-22 08:07:19 +01:00
Burkhart Wolff 8771d8581b default class checking bug fixed; new attributes for default classes in ontological macros Definition* Theorem* Lemma* 2020-12-01 23:18:13 +01:00
Burkhart Wolff 698da3dd24 intermediate session with Macro-Bug. 2020-11-24 10:57:17 +01:00
Burkhart Wolff efeee1e863 Eliminated deprecated abstract class residuals; lifted Definition* to math_content. 2020-11-10 13:07:54 +01:00
Burkhart Wolff 2ecb62a80e added Lemma*, Theorem* and Definition* support. Bug: referencing does not work. 2020-11-04 15:55:43 +01:00
Burkhart Wolff 7f4b587274 steps to reform cicm/csp paper and manual 2020-11-04 11:18:43 +01:00
Burkhart Wolff dc7ed74c57 Second steps to reform cicm paper 2020-11-04 10:12:31 +01:00
Burkhart Wolff 84c7cabec0 First steps to reform cicm paper 2020-11-04 09:22:49 +01:00
Burkhart Wolff fbefa85586 First steps to reform cicm paper 2020-11-04 03:27:24 +01:00
Burkhart Wolff c991e693dc tested and enforced new author* and abstract* macros. 2020-11-04 02:52:55 +01:00
Achim D. Brucker 0b52e5872d Use author*. 2020-11-03 21:50:19 +00:00
Burkhart Wolff bad7dfc2ef new set of macros : author* and abstract* --- not working yet 2020-11-03 19:00:33 +01:00
Burkhart Wolff fe8f63690d macro-arrangement ... 2020-11-02 18:30:40 +01:00