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,367 Commits 15 Branches 8 Tags 73 MiB
Commit Graph

639 Commits

Author SHA1 Message Date
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). 2022-03-26 21:31:05 +00:00
Achim D. Brucker 21ab0ff6b9 Removed reference to Docker use. 2022-03-26 20:08:17 +00:00
Achim D. Brucker f4286404fb Merge branch 'v1.2.x/Isabelle2021' 2022-03-26 18:25:33 +00:00
Achim D. Brucker a1d83e33ef Updated manual to reflect changes in options for install script. 2022-03-26 18:23:07 +00:00
Achim D. Brucker 1a41e92188 Minor shortenings to improve layout. 2022-03-26 17:47:40 +00:00
Achim D. Brucker 5381182ab2 Spell-checking. 2022-03-26 13:26:51 +00:00
Achim D. Brucker 76582f75fd Merge branch 'master' into porting_to_Isabelle2021-1 2022-03-23 14:33:44 +00:00
Nicolas Méric a4f39bb700 Add TODO referring to an issue in DOF Manual 
Reference the issue
Isabelle_DOF/Isabelle_DOF#10
in a TODO in the DOF manual to remember to update the manual
when the issue is fixed
 2022-03-23 11:27:11 +01:00
Nicolas Méric 13835fbed9 Fix typos in DOF manual, chapter 5 2022-03-23 11:17:30 +01:00
Nicolas Méric cc3f9ab402 Update DOF manual, chapter 3 and 4 
- Use antiquotations when possible to reference
  classes and attributes in text (typ, type and const antiquotations)
- Add explanation for cid, obj-id and oid
- Update ML*, text* an value* railroads
- Fix typos
- Add some TODOs for the next revision of the manual
 2022-03-23 09:07:43 +01:00
Achim D. Brucker 442835442f Towards Isabelle 2021-1 support. 2022-03-22 22:19:35 +00:00
Achim D. Brucker c69b11a312 First steps towards Isabelle 2021-1 support. 2022-03-22 21:47:26 +00:00
Achim D. Brucker 0c9dcfb6e1 Merge branch 'master' into porting_to_Isabelle2021-1 2022-03-21 20:32:19 +00:00
Nicolas Méric 5d0136a168 Fix typo in DOF Manual, Chapter 3 2022-03-21 14:15:09 +01:00
Nicolas Méric 3e9adb026b Update DOF manual Chapter 3 
- Fix some minor issues:
  - Some figures did not longer correspond to their descriptions
  - Some mechanisms (definitions - examples - etc.) in referencing
    did not work any longer in the setting that we distribute.
- Fix typos
 2022-03-21 14:09:18 +01:00
Achim D. Brucker 2314b2191f Resolved merge conflict. 2022-03-20 20:49:46 +00:00
Burkhart Wolff 6bb62fb08a minor presentation bug 2022-03-20 19:04:52 +01:00
Burkhart Wolff fb91700a43 added a remark on @{cite ...} 2022-03-20 19:02:14 +01:00
Burkhart Wolff d86173834f merge 2022-03-20 18:47:18 +01:00
Burkhart Wolff 49f4c5b95b added hacky para on alternative lexical notations. 2022-03-20 18:45:53 +01:00
Achim D. Brucker 658e7a68a1 Disabled non-working antiquotation - needs to have a second look. 2022-03-20 14:57:03 +00:00
Achim D. Brucker bdc7aab6cf Minor syntax cleanup. 2022-03-20 14:55:56 +00:00
Achim D. Brucker 90416c2310 Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF 2022-03-18 20:29:35 +00:00
Achim D. Brucker 36c0e415e3 Made use of hvlogos.sty optional. 2022-03-18 20:29:22 +00:00
Burkhart Wolff 2ca84fd40f Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF 2022-03-18 19:20:29 +01:00
Burkhart Wolff 306d117231 ... 2022-03-18 19:20:25 +01:00
Nicolas Méric b7d7015423 Cleanup Manual chapter 03 2022-03-17 17:28:40 +01:00
Nicolas Méric e4195a68a2 Update DOF manual, chapters 02-03 
- Use antiquotations when possible to reference
  classes and attributes in text (typ and const antiquotations)
- Update some isar code examples
- Fix typos
 2022-03-17 17:14:20 +01:00
Achim D. Brucker 54c9bc2d74 Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF 2022-03-17 08:56:41 +00:00
Achim D. Brucker f6e9e39a58 Removed reference to lncs as a special case, as llncs.cls finally arrived on CTAN. 2022-03-17 08:51:37 +00:00
Nicolas Méric 3585b6a2f1 Explain queries on instances in DOF manual 2022-03-15 08:28:10 +01:00
Nicolas Méric 3895ba550c Import of DOF manual changes from /2021-ITP-PMTI 2022-03-14 17:08:59 +01:00
Achim D. Brucker 53eb93367c Cleanup. 2022-03-11 10:41:06 +00:00
Achim D. Brucker 005d18657c Switched to hvlogos. 2022-03-11 07:40:07 +00:00
Achim D. Brucker 6cf004637c Removed ITP paper draft - on own branch. 2022-03-11 07:24:54 +00:00
Achim D. Brucker 462673d31e Removed math example (outdated and currently unused). 2022-03-11 07:24:14 +00:00
Achim D. Brucker 43522215b9 Removed empty README. 2022-03-11 07:14:35 +00:00
Nicolas Méric 8f7e898f4b Fix invariant railroad diagram 2022-01-31 13:01:59 +01:00
Nicolas Méric 76612ae6f3 Add checking of invariants for class instances 
- Warning: the current implementation does yet not support
    some use-cases, like invariant on monitors,
    or the initialization of docitem without a class associated.
- Add first draft of the checking of invariants.
  For now, it is disabled by default because some cases
  are not yet supported, like the initialization of docitem
  without a class associated.
  ex: text*[sdf]‹ Lorem ipsum @{thm refl}›
- To enable the checking, one can use the theory attribute
  "invariants_checking" by declaring it in a theory like this:
  declare [[invariants_strict_checking = true]]
- A checking using basic tactics (unfolding and auto) can be enable
  with the "invariants_checking_with_tactics" theory attribute
  for specific use-cases
- The specification of invariants is now automatically abstracted,
  so one must define an invariant like this now:

  doc_class W =
  w::"int"
  invariant w :: "w σ ≥ 3"

  The old form:

  doc_class W =
  w::"int"
  invariant w :: "λσ. w σ ≥ 3"

  is now deprecated.
  The specification of the invariant still uses the σ-notation
  and is defined globally by the name component "invariantN"
- Update the invariants definition in the theories to match
  the new implementation
- Update the manual to explain this new feature
- Add small examples in src/tests/High_Level_Syntax_Invariants.thy
  and src/tests/Ontology_Matching_Example.thy
 2022-01-24 17:30:48 +01:00
Burkhart Wolff 96112ff893 restored ancient SEFM paper example for invariants 2022-01-17 12:06:32 +01: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 86b555b56e Disable TR_my_commented_isabelle for now: does not work with Isabelle2021-1. 2021-12-18 23:07:25 +01:00