 Achim D. Brucker
|
9feeb63665
|
Linting ...
|
2024-04-26 07:00:44 +01:00 |
|
Achim D. Brucker
|
55e42142fa
|
Spell Checking.
|
2024-04-26 02:32:25 +01:00 |
 Burkhart Wolff
|
7d6048bf64
|
Merge branch 'afp_resubmission' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF into afp_resubmission
|
2024-04-16 11:11:07 +02:00 |
|
Burkhart Wolff
|
231892cd23
|
...
|
2024-04-16 11:11:04 +02:00 |
Nicolas Méric
|
c945da75fa
|
Proof reading
|
2024-04-15 14:28:31 +02:00 |
|
Nicolas Méric
|
b554f20a5c
|
Move onto_morphism command to isabelle dof core
|
2024-04-15 12:57:42 +02:00 |
|
Burkhart Wolff
|
734c1953bd
|
polishing
|
2024-04-12 18:52:57 +02:00 |
|
Burkhart Wolff
|
a735e9a1f2
|
roughly complete section 5 on proofs over ontologies.
|
2024-04-12 18:42:04 +02:00 |
Burkhart Wolff
|
7c2a6099f8
|
section on previewer
|
2024-04-11 21:08:36 +02:00 |
|
Burkhart Wolff
|
6dfefc6b4e
|
some elements in the proof chapter
|
2024-04-09 09:27:14 +02:00 |
|
Burkhart Wolff
|
3235410af3
|
some elements of chapter Proof_Ontologies.
|
2024-04-07 22:07:40 +02:00 |
|
Burkhart Wolff
|
4745c58803
|
some elements of chapter Proof_Ontologies.
|
2024-04-07 22:04:09 +02:00 |
|
Burkhart Wolff
|
28d1fa926e
|
Merge branch 'main' into afp_resubmission
|
2024-04-07 17:19:24 +02:00 |
|
Burkhart Wolff
|
b651116af3
|
nicer presentation of proofs, closer to automation.
|
2024-04-05 15:23:33 +02:00 |
|
Nicolas Méric
|
93ef94cddb
|
Move some theorems in regexpinterface
|
2024-04-05 14:56:55 +02:00 |
|
Nicolas Méric
|
20e90f688f
|
Merge branch 'main' into afp_resubmission
|
2024-04-05 14:30:03 +02:00 |
|
Burkhart Wolff
|
02b6d0b048
|
towards mechanization.
|
2024-04-05 13:40:44 +02:00 |
|
Burkhart Wolff
|
f5a94ca962
|
completed proofs wrt. ordered Language of monitors.
|
2024-04-04 21:27:20 +02:00 |
|
Burkhart Wolff
|
6b2879d1d6
|
bric a brac
|
2024-04-04 15:52:26 +02:00 |
|
Nicolas Méric
|
51d93e38f8
|
Add constants for first monitor accepts clause
|
2024-04-04 12:08:35 +02:00 |
|
Nicolas Méric
|
7791538b54
|
Update to isabelle 2023 and add morphism examples
|
2024-04-04 12:08:25 +02:00 |
|
Burkhart Wolff
|
dee3b47d06
|
some more lemmas
|
2024-04-04 10:08:41 +02:00 |
|
Burkhart Wolff
|
0bf21336f1
|
cleanup
|
2024-04-03 21:10:53 +02:00 |
|
Burkhart Wolff
|
2b12e53cf4
|
first monitor proof without sorries.
|
2024-04-03 20:51:21 +02:00 |
|
Burkhart Wolff
|
c2eea7696b
|
...
|
2024-04-03 16:15:29 +02:00 |
|
Burkhart Wolff
|
20f163eba9
|
experiments
|
2024-04-03 15:01:25 +02:00 |
|
Burkhart Wolff
|
2d2cb6c8ce
|
some experiments on monitor proofs-
|
2024-04-02 23:50:32 +02:00 |
|
Nicolas Méric
|
291b2e258f
|
Use name spaced names for docitem_name text anti-quotation
|
2024-03-12 18:21:53 +01:00 |
|
Nicolas Méric
|
1740898171
|
Add message for matching error in class invariants
Give feedback for not well formed class invariants
|
2024-03-01 17:24:12 +01:00 |
|
Nicolas Méric
|
41dd3e4949
|
Update output latex macros name
Allow instance names compatible with binding names,
including names with subscripts
|
2024-02-29 10:16:51 +01:00 |
|
Achim D. Brucker
|
c4875da7cb
|
Removed (non-working) support for eptcs.
|
2024-02-25 11:45:46 +00:00 |
|
Achim D. Brucker
|
a286e4b1bc
|
Improved dof_mkroot setup and minor LaTeX fixes.
|
2024-02-25 11:38:43 +00:00 |
|
Nicolas Méric
|
207029e70e
|
Enable term anti-quotations in class invariants
|
2024-02-14 11:15:13 +01:00 |
|
Achim D. Brucker
|
645a3edcec
|
Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
|
2024-02-08 19:23:56 +00:00 |
|
Achim D. Brucker
|
572ec2d0bb
|
Use providecommand instead of usecommand to preserve already existing definition.
|
2024-02-08 19:20:09 +00:00 |
|
Nicolas Méric
|
d59dabaf7c
|
Cleanup
|
2024-02-06 11:01:16 +01:00 |
|
Nicolas Méric
|
e78a114879
|
Fix typo
ci/woodpecker/push/build Pipeline failed
Details
|
2023-11-27 12:01:52 +01:00 |
|
Burkhart Wolff
|
443d63f3b5
|
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
ci/woodpecker/push/build Pipeline failed
Details
|
2023-11-25 17:06:39 +01:00 |
|
Nicolas Méric
|
331fcd07f0
|
Update invariants checking
ci/woodpecker/push/build Pipeline failed
Details
Make invariants checking compatible with namespaces
and the new invariants implementation
|
2023-11-20 16:57:01 +01:00 |
|
Nicolas Méric
|
5dc20889a8
|
Partially implement polymorphic classes support for class invariants
ci/woodpecker/push/build Pipeline failed
Details
|
2023-11-08 08:47:54 +01:00 |
|
Burkhart Wolff
|
e2b3184a77
|
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
|
2023-09-21 04:58:34 +02:00 |
|
Nicolas Méric
|
7b54bf5ca5
|
Cleanup
ci/woodpecker/push/build Pipeline failed
Details
|
2023-09-20 15:56:50 +02:00 |
|
Nicolas Méric
|
baa36b10c1
|
Cleanup
ci/woodpecker/push/build Pipeline failed
Details
|
2023-09-20 15:00:43 +02:00 |
|
Nicolas Méric
|
c57ce6292b
|
Update output type name for latex refs
ci/woodpecker/push/build Pipeline failed
Details
|
2023-09-19 17:03:00 +02:00 |
|
Achim D. Brucker
|
e12abadc94
|
Test with Isabelle 2023.
ci/woodpecker/push/build Pipeline failed
Details
|
2023-09-14 06:29:01 +01:00 |
|
Achim D. Brucker
|
792fd60055
|
Merge branch 'main' into isabelle_nightly
ci/woodpecker/push/build Pipeline failed
Details
|
2023-09-12 18:58:58 +01:00 |
|
Nicolas Méric
|
ec7297f1d3
|
Update instances list term antiquotation
ci/woodpecker/push/build Pipeline failed
Details
Make instances list term antiquotation compatible with
polymorphic classes
|
2023-09-11 09:07:10 +02:00 |
|
Achim D. Brucker
|
e4ee3ff240
|
Merge branch 'main' into isabelle_nightly
ci/woodpecker/push/build Pipeline was successful
Details
|
2023-08-31 08:27:53 +01:00 |
|
Achim D. Brucker
|
4393042f2c
|
Merge.
ci/woodpecker/push/build Pipeline was successful
Details
|
2023-08-29 08:09:28 +01:00 |
|
Achim D. Brucker
|
fef7b9d60b
|
Merge commit 'cef4086029' into isabelle_nightly
ci/woodpecker/push/build Pipeline failed
Details
|
2023-08-29 06:40:37 +01:00 |