Achim D. Brucker
abe7713f1e
Disabled patch installation and updated Isabelle version.
2022-03-20 22:03:10 +00: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
50e42ca5c0
Reorganized CI setup.
2022-03-20 11:04:23 +00:00
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