Burkhart Wolff
63c0b1e442
cosmetics in Evaluation
2022-03-16 13:25:56 +01:00
3585b6a2f1
Explain queries on instances in DOF manual
2022-03-15 08:28:10 +01:00
8bc2e60d2f
Update high level invariants tests
2022-03-14 18:44:09 +01:00
3895ba550c
Import of DOF manual changes from /2021-ITP-PMTI
2022-03-14 17:08:59 +01:00
eb9edd66d5
Clean up code
2022-03-14 16:17:28 +01:00
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
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
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: #8
2022-01-25 07:50:25 +00:00
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
4352691e95
Support Isabelle2021-1 without patches:
...
in the next release it will be simpler again.
2021-12-20 21:02:57 +01:00
Makarius Wenzel
2547b2324e
Adhoc examples for ML antiquotations.
2021-12-20 16:27:16 +01:00
Makarius Wenzel
99264edc02
More NOTES.
2021-12-20 09:22:13 +01:00
Makarius Wenzel
70617f59fe
Avoid pointless Latex comments: as an example of how to re-define document output.
2021-12-19 17:51:38 +01:00
Makarius Wenzel
fadd982285
More on Isabelle/Scala services, notably document preparation.
2021-12-19 17:16:37 +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
Makarius Wenzel
2e4d37e3ca
More on Document preparation in Isabelle/ML.
2021-12-19 15:23:33 +01:00
Makarius Wenzel
ff32bac3fc
Miscellaneous NEWS and Notes.
2021-12-19 13:48:45 +01:00
Burkhart Wolff
96d6bb8e00
intro proposal completed
2021-12-19 13:31:42 +01:00
Makarius Wenzel
bcf7849083
Proper component setup.
2021-12-19 13:22:07 +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
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
6c99612dcd
Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2021-12-16 13:49:49 +01:00
Burkhart Wolff
3f09aca090
added paper frame, small things.
2021-12-16 13:49:44 +01:00
Achim D. Brucker
9632c0810b
Merge pull request 'clean-up-isa-check-functions' ( #7 ) from nicolas.meric/Isabelle_DOF:clean-up-isa-check-functions into master
...
Reviewed-on: #7
2021-12-15 22:25:28 +00:00
Achim D. Brucker
a2673b0825
Merge branch 'master' into clean-up-isa-check-functions
2021-12-15 22:25:22 +00:00
Achim D. Brucker
546b4fbcfe
Merge pull request 'Add the possibility to make request on instances' ( #6 ) from nicolas.meric/Isabelle_DOF:request-on-instances-first-draft into master
...
Reviewed-on: #6
2021-12-15 22:25:03 +00:00
Burkhart Wolff
Nicolas Méric
Achim D. Brucker
Nicolas Méric
Makarius Wenzel