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

1303 Commits

Author SHA1 Message Date
Achim D. Brucker d7cf6f1fc7 Removed outdated Jenkinsfile. 2022-03-19 21:07:12 +00:00
Achim D. Brucker a89878079e Generate link to latest artifacts. 2022-03-19 20:29:22 +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 2886f7df99 Update CENELEC_50128 theory 
An application condition should be an assumption
 2022-03-18 17:00:06 +01:00
Achim D. Brucker 703b9a055d Renamed build step. 2022-03-17 22:32:35 +00:00
Achim D. Brucker a950142749 Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF 2022-03-17 22:28:49 +00:00
Achim D. Brucker 6c74a2e0f5 Basic Woodpecker setup (migration from Jenkins). 2022-03-17 22:28:31 +00: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
Achim D. Brucker a66e90cf25 Switchted to notion of upstream repository. 2022-03-17 08:48:25 +00:00
Burkhart Wolff 63c0b1e442 cosmetics in Evaluation 2022-03-16 13:25:56 +01:00
Nicolas Méric 3585b6a2f1 Explain queries on instances in DOF manual 2022-03-15 08:28:10 +01:00
Nicolas Méric 8bc2e60d2f Update high level invariants tests 2022-03-14 18:44:09 +01:00
Nicolas Méric 3895ba550c Import of DOF manual changes from /2021-ITP-PMTI 2022-03-14 17:08:59 +01:00
Nicolas Méric eb9edd66d5 Clean up code 2022-03-14 16:17:28 +01:00
Nicolas Méric a332109dca Fix scheduling problem for term* and value* 
Toplevel transition only allows atomic transactions.
So we avoid sequantial combinators
 2022-03-14 15:27:13 +01:00
Burkhart Wolff 5af219469d Corrected scheduling problem of ML*. must be atomic transaction. 2022-03-14 12:23:54 +01:00
Achim D. Brucker 17d7562d4f Updated year. 2022-03-11 11:43:02 +00:00
Achim D. Brucker 8efc1300b4 Manual import of changes from /2021-ITP-PMTI. 2022-03-11 11:30:34 +00:00
Achim D. Brucker 4c0d3ccee3 Renamed master repository to main repository. 2022-03-11 10:42:50 +00: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
Burkhart Wolff e650892b48 changed 'L' - operator to 'Lang' in order to avoid name conflicts in papers. 2022-01-31 10:44:02 +01:00
Burkhart Wolff 35b47223b9 added category 'background' into scholarly paper 2022-01-31 10:42:52 +01:00
Achim D. Brucker 46325cc64b Added unofficial support for lipics-v2021 (warning: this requires a patched version of lipics-v2021.cls). 2022-01-30 22:52:48 +00:00
Nicolas Méric d546a714b7 Merge pull request 'Add checking of invariants for class instances' (#8) from nicolas.meric/Isabelle_DOF:check-invariants-first-draft into master 
Reviewed-on: Isabelle_DOF/Isabelle_DOF#8
 2022-01-25 07:50:25 +00: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
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
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 6c99612dcd Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF 2021-12-16 13:49:49 +01:00