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
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
Burkhart Wolff
9b08e92588
Experiments with the code generator for Isa_DOF class objects.
2021-10-08 16:00:57 +02:00
Burkhart Wolff
5f47588270
added some value-statements for demonstration purposes
2021-10-05 16:22:05 +02:00
Burkhart Wolff
eb292a695b
added poor man's encoding of inheritance in Cyto-Model.
2021-10-04 15:11:29 +02:00
Burkhart Wolff
3f8880c0f0
added small fun ontology for examples : Cytology
2021-09-29 14:08:28 +02:00
Nicolas Méric
f11e5b762b
all changes
2021-06-01 14:51:22 +02:00
Burkhart Wolff
f8801a1121
basically table_inline.
2021-05-13 14:37:27 +02:00
Achim D. Brucker
920779b150
Raised requirement of Tex Live to TeX Live 2021 (expected release date: 4th of April 2021).
2021-03-22 00:13:18 +00:00
Achim D. Brucker
712cea7ac9
Merge branch 'v1.1.x/Isabelle2020'
2021-03-20 22:26:14 +00:00
Achim D. Brucker
a0654d8db9
Added Nicolas Méric as contributor.
2021-03-20 22:05:57 +00:00
Achim D. Brucker
e048bbe508
Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
2021-03-15 10:25:16 +00:00
Achim D. Brucker
201d12a01a
Fixed spelling.
2021-03-15 10:24:58 +00:00
Burkhart Wolff
cfad21e296
Ref auf Makarius Text added
2021-03-14 15:45:42 +01:00
Achim D. Brucker
389fd6d033
Switch from pdf(la)tex to lua(la)tex.
2021-03-10 23:51:18 +00:00
Achim D. Brucker
f975672901
Removed check for \expanded{}: Isabelle 2021 defaults to luatex as TeX-engine, which has \expanded{} since a very long time.
2021-03-10 22:12:39 +00:00
Achim D. Brucker
06dddeacf5
Porting to Isabelle 2021.
2021-03-10 22:04:09 +00:00
Achim D. Brucker
e495a7b2fe
Revising Chapter 5.
2021-02-13 17:04:17 +00:00
Achim D. Brucker
018bfa4bcd
Added default escapechar for ltx environment.
2021-02-12 02:24:31 +00:00
Achim D. Brucker
15c958ec64
Revised Chapter 4.
2021-02-11 19:10:38 +00:00
Achim D. Brucker
29661f6734
Revised Sec. 4.2.
2021-02-10 09:05:59 +00:00
Achim D. Brucker
3649fb855e
Revised Sec. 4.1.
2021-02-09 20:56:56 +00:00
Achim D. Brucker
43184a9995
Migrated \inlinebawsh{}.
2021-02-08 15:34:59 +00:00
Achim D. Brucker
ed8cd2ad9d
Migrated \inlinebawsh{}.
2021-02-08 15:33:45 +00:00
Achim D. Brucker
029ae709e6
Migrated \inlineltx{}, except when argument contained { or }.
2021-02-07 20:01:43 +00:00
Achim D. Brucker
85d94848b6
Revised Chapter 3.
2021-02-06 12:08:18 +00:00
Achim D. Brucker
b61346fd64
Revised Sec. 3.2.
2021-02-05 06:58:22 +00:00
Achim D. Brucker
3d0cbf6a4f
Revised Sec. 3.1.
2021-02-04 18:52:38 +00:00
Achim D. Brucker
50d3dde1a0
Converted \inlinesml{...}.
2021-02-03 05:13:05 +00:00
Achim D. Brucker
d605e23218
Converted \inlinesml{...}.
2021-02-02 12:22:35 +00:00
Achim D. Brucker
2d3e521296
Converted \inlinebash{...}.
2021-02-02 12:20:03 +00:00
Achim D. Brucker
b81eef7bd2
Converted bash-environments to antiqotations.
2021-02-01 05:06:15 +00:00
Achim D. Brucker
a1332ec9a4
Converted bash-environments to antiqotations.
2021-01-31 16:54:22 +00:00
Achim D. Brucker
243556467a
Merge remote-tracking branch 'origin/add-todos-fix-typos'
2021-01-30 06:47:47 +00:00
Nicolas Méric
4d9de40037
Add TODOs to improve the wording
2021-01-28 13:04:29 +01:00
Nicolas Méric
76266fbd5e
Add TODOs to improve text consistency
...
There are some inconsistencies between some figures and the text
which refers to them.
2021-01-28 12:59:48 +01:00
Nicolas Méric
1fb97c8fb0
Add TODOs to delete references to where clause
...
The where clause for ontology classes is deprecated
in favor of the accepts and rejects clauses.
2021-01-28 12:48:54 +01:00
Nicolas Méric
5b618562a2
Fix some typos
2021-01-28 12:46:20 +01:00
Achim D. Brucker
e9fc175cb6
Cleanup.
2021-01-25 23:34:23 +00:00
Achim D. Brucker
7e3c82f65e
Cleanup.
2021-01-21 16:20:27 +00:00
Achim D. Brucker
b4482b02d9
Modernized comment syntax.
2021-01-20 23:25:17 +00:00
Achim D. Brucker
a9737762fd
Fixed spacing in front of index entries..
2021-01-19 23:12:58 +00:00
Achim D. Brucker
fc2817db0d
Cleanup.
2021-01-18 20:30:39 +00:00
Achim D. Brucker
6ed771ef04
Workaround to support lualatex.
2021-01-17 06:37:14 +00: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
7e01ff7021
Cleanup.
2021-01-08 03:54:37 +00:00
Achim D. Brucker
82121d7204
Cleanup.
2021-01-07 04:39:28 +00:00
Achim D. Brucker
225309482b
Updated copyright information.
2021-01-06 06:48:36 +00:00
Achim D. Brucker
78a17a66b5
Fixed copyright header.
2021-01-05 11:32:26 +00:00
Achim D. Brucker
20b3e7c0b7
Removed pdflatex check (TeX Live 2019 should available everywhere and the dependency is still checked during installation.
2021-01-05 11:25:55 +00:00
Achim D. Brucker
d2dcc71229
Removed explicit vspaces to clean up layout.
2021-01-04 06:32:56 +00:00
Burkhart Wolff
d86e708154
a first imprfect solution for the assert* problem; 4th chapter roughly completed.
2021-01-03 14:07:21 +01:00
Burkhart Wolff
aee1d33709
renaming ISA's; new shortcuts; more content in the RefMan.
2021-01-02 15:57:28 +01:00
Burkhart Wolff
b71be9c4a8
Reorganization Chap 4. <4.3.2
2021-01-01 21:34:05 +01:00
Burkhart Wolff
396ef1d477
More content in 4, better tree printing.
2021-01-01 21:23:21 +01:00
Burkhart Wolff
950a86aa5a
Adding better explanation of the core functionalities...
2021-01-01 16:12:07 +01:00
Burkhart Wolff
480f0ada37
Reorganization Chap 4. ...
2020-12-31 11:02:27 +01:00
Burkhart Wolff
242bb536bc
Reorganization Chap 4. <4.3.2
2020-12-30 23:07:19 +01:00
Burkhart Wolff
d6832cc8f8
Reorganization Chap 4.
2020-12-30 15:06:11 +01:00
Burkhart Wolff
04f0cc7f5c
Reorganization: Pushed Macro Core Mechanism into the DOF Core; adapted the RefMan accordingly.
2020-12-30 12:47:54 +01:00
Burkhart Wolff
2f721d0f4b
activated syntactic checks for trimming macros
2020-12-24 04:53:27 +01:00
Burkhart Wolff
4c5aacb39f
activated syntactic checks for trimming macros
2020-12-23 11:30:42 +01:00
Burkhart Wolff
005922ffda
built in syntactic checks for trimming macros
2020-12-23 09:41:26 +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
0e64608a58
enforcing shorter Definition* - style in examples (CC,CENELEC,...)
2020-12-02 09:32:48 +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
da0f3e63f1
more steps to reform document macro mechanism
2020-11-04 13:13:24 +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
Burkhart Wolff
1f403a09f6
dfg
2020-11-02 14:14:52 +01:00
Burkhart Wolff
abd32a802d
First Pass of Chap 4 - Added invariant syntax description, more semantic content
2020-10-26 12:27:33 +01:00
Burkhart Wolff
f093b033f5
started pass on chap 4 in Refman.
2020-10-26 10:08:22 +01:00
Burkhart Wolff
3ba9454ac7
Slight improvements of the layout
2020-10-25 12:57:43 +01:00
Burkhart Wolff
3c6197e6ca
FINISHED MY PASS ON THE PROGRAMMING MANUAL.
2020-10-25 12:02:44 +01:00
Burkhart Wolff
7999ee9a38
recvision till line 2000 (Term Parsing)
2020-10-21 13:49:01 +02:00
Burkhart Wolff
9b2c08183e
recvision till line 2000 (Term Parsing)
2020-10-20 18:26:20 +02:00
Burkhart Wolff
9ad51e9d70
Actualized Para on Toplevel Management
2020-10-20 14:22:53 +02:00
Achim D. Brucker
538292b972
Fixed LaTeX compiliation error.
2020-10-06 04:45:30 +01:00
Burkhart Wolff
c554b12be2
minor embellishments
2020-09-29 10:15:12 +02:00
Burkhart Wolff
873eda8ee0
stiluebungen
2020-09-25 13:38:34 +02:00
Burkhart Wolff
cdc1e0a7d8
stiluebungen < 1150
2020-09-23 13:57:32 +02:00
Burkhart Wolff
2cdf9f3124
stiluebungen < 1150
2020-09-23 13:23:20 +02:00
Burkhart Wolff
bea648530b
pushup.
2020-09-22 16:57:50 +02:00
Burkhart Wolff
d655effcf8
pushup.
2020-09-22 16:47:05 +02:00
Burkhart Wolff
9956bbf062
pushup, stiluebungen.
2020-09-22 16:35:28 +02:00
Burkhart Wolff
c1d6694b7c
stiluebungen am PML
2020-09-22 14:50:57 +02:00
Burkhart Wolff
ad6ba9e302
stiluebungen am PML
2020-09-21 21:24:08 +02:00
Burkhart Wolff
6f36efae7f
stiluebungen am PML
2020-09-21 19:41:47 +02:00
Burkhart Wolff
b9de7663b6
added some paras in Guided Tour, corrected figure config Bug, exercice de style in MyCommentedIsa
2020-09-19 12:49:37 +02:00
Burkhart Wolff
6c6644ae0c
Updated MyCommentedIsabelle (a little; finished Guided Tour
2020-09-18 17:01:49 +02:00
Burkhart Wolff
5c22b80fb4
Nearly complete pass through chap 3
2020-09-16 14:24:39 +02:00
Achim D. Brucker
137262890e
Improved 'verbatim' output (removed generated %-signs).
2020-09-15 07:28:32 +01:00
Burkhart Wolff
41ac6006f8
rough pass through the guided tour.
2020-09-09 16:51:59 +02:00
Burkhart Wolff
2f95c56060
Version mit LaTeX Bizarrerie - verbatim _
2020-09-09 14:54:09 +02:00
Burkhart Wolff
2d2f4320e0
intermediate status with LaTeX pblsm
2020-09-09 13:17:22 +02:00
Achim D. Brucker
58617e87e6
Conversion: \isadof -> \<^isadof>.
2020-09-08 13:45:09 +01:00
Achim D. Brucker
640929ea71
Removed listings-based Isar setup.
2020-09-08 07:41:09 +01:00
Achim D. Brucker
37a71a613e
Ad hoc conversion: \inlineisar|...| -> @{boxed_theory_text ... }.
2020-09-08 07:30:14 +01:00
Achim D. Brucker
3dabf4fc82
Improvements: @{boxed_theory_text [display] ... }.
2020-09-08 06:51:36 +01:00
Achim D. Brucker
109802a76a
Ad hoc conversion: \begin{isar}...\end{isar} -> @{boxed_theory_text [display] ... }.
2020-09-08 06:18:01 +01:00
Achim D. Brucker
6c2ad62df2
Cleanup.
2020-09-08 00:11:22 +01:00
Achim D. Brucker
ee251a8000
Removed unused LaTeX definitions and style files.
2020-09-08 00:01:50 +01:00
Achim D. Brucker
7956a3009a
Initial commit: style for providing theorem-like default environments.
2020-09-07 23:56:43 +01:00
Achim D. Brucker
75719a933a
Added 2020-iFM-CSP example based on scrartcl.cls.
2020-09-07 23:35:43 +01:00
Achim D. Brucker
6b4bd6fea4
Removed boxed isar.
2020-09-07 23:19:41 +01:00
Burkhart Wolff
685f020b22
more content in Guided Tour.
2020-09-07 23:17:36 +01:00
Burkhart Wolff
39efc61686
some inpuit on Guided Tour
2020-09-07 23:17:36 +01:00
Burkhart Wolff
2321945dc4
sdf
2020-09-07 23:17:36 +01:00
Burkhart Wolff
fd532d985a
activated the new markup wherever possible. Started to revise chap 3.
2020-08-28 17:41:16 +02:00
Burkhart Wolff
094281cf89
added wrapper to achims listings environments.
2020-08-28 12:42:20 +02:00
Burkhart Wolff
d206bf9f7c
shifted new env up into COL. Declared in the Frontmatter.
2020-08-27 15:54:51 +02:00
Burkhart Wolff
38ba8cace0
brought experiments with generic sub-text-element-environments into shape
2020-08-27 14:08:49 +02:00
Burkhart Wolff
b3ff21e210
introducing and testing of macros bindex and index.
2020-08-26 17:08:45 +02:00
Burkhart Wolff
41a1eaed44
added define_macros, corrections in 02_Background
2020-08-26 14:38:39 +02:00
Burkhart Wolff
1dd07880ea
inbtroduced shortcut interface.
2020-08-26 09:56:25 +02:00
Burkhart Wolff
7a768cfdeb
versatile
2020-08-26 08:43:39 +02:00
Burkhart Wolff
338bb7d4a4
Code cleanup.
2020-08-25 11:59:10 +02:00
Burkhart Wolff
a792cc79d2
was lucky to solve a deep bug in standard antiquotation evaluation inside text* soon.
2020-08-25 11:11:38 +02:00
Burkhart Wolff
f239b36b49
Reworked textually abstract, intro, background. Eliminate \emph
2020-08-25 09:17:36 +02:00
Burkhart Wolff
7cb6577797
solved presentation bug (brown) and eliminated some code dups
2020-08-24 11:33:32 +02:00