6c588c3fe4
added diag 'integrated document'
ci/woodpecker/push/build Pipeline was successful
Details
2023-04-14 10:41:14 +02:00
36cd3817cf
Quick fix for text* macros latex output
ci/woodpecker/push/build Pipeline was successful
Details
2023-04-11 18:52:57 +02:00
Burkhart Wolff
8c6abf2613
...
ci/woodpecker/push/build Pipeline was successful
Details
2023-04-05 16:46:21 +02:00
Achim D. Brucker
698e6ab169
Bug fix: document variants.
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-29 22:21:44 +01:00
Achim D. Brucker
320614004e
Improved LaTeX support for Lemma*, Theorem*, Definition*, etc.
2023-03-29 22:21:22 +01:00
91ff9c67af
repaired some obvious errors in sty - still incomplete
ci/woodpecker/push/build Pipeline failed
Details
2023-03-29 11:41:30 +02:00
1838baecb9
some revision of ITP paper
ci/woodpecker/push/build Pipeline failed
Details
2023-03-28 09:54:16 +02:00
accc4f40b4
Improved Testset for new ontology elements
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-26 20:58:55 +02:00
4ba0c705b4
deactivated CENELEC in tests (nothing tested, just time consumed)
2023-03-26 20:56:54 +02:00
5d89bcc86a
added some demonstrations/tests
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-25 10:49:50 +01:00
07527dbe11
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2023-03-24 17:22:49 +01:00
81a50c6a9e
Reactivating failing assertions
2023-03-24 17:21:36 +01:00
5628eaa2dc
Code Cleanup
2023-03-24 17:20:45 +01:00
230247de1a
Update Manual and code
...
ci/woodpecker/push/build Pipeline was successful
Details
- Update term context section
- Add option to define a default class for declare_reference*
- Use defined symbol identifiers \<quote> and \<doublequote>
to simplify caveat section about lexical conventions
- Rename Manual theories to avoid issues
when using Syntax.parse_term that is not compatible with
with long-names staring with a number or an underscore
- Rewrite names used as mixfix annotation
for the term-antiquotations to rule out
mixform form excluded symbols
2023-03-24 17:02:24 +01:00
0834f938a9
code cleanup
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-24 12:59:54 +01:00
63c2acfece
improved title setup for testSuite
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-24 10:41:32 +01:00
3a4db69184
updated Evaluation Section
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-24 08:28:14 +01:00
3fc4688f69
updated Evaluation Section
ci/woodpecker/push/build Pipeline failed
Details
2023-03-24 08:13:51 +01:00
7dbd016b5d
Pass throúgh evaluations
2023-03-24 08:08:55 +01:00
3b446c874d
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2023-03-21 14:33:25 +01:00
4de23de5ee
...
2023-03-21 14:33:21 +01:00
4bd31be71d
Remove obsolete termrepr term anti-quotation
...
ci/woodpecker/push/build Pipeline was successful
Details
- Also some clean-up
2023-03-20 16:50:23 +01:00
5ad6c0d328
Add getters and mappings for name-spaced objects
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-17 14:05:05 +01:00
Achim D. Brucker
5292154687
Converted é to \'e to work around the lack of first-class unicode support.
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-15 12:15:08 +00:00
Achim D. Brucker
caf966e3df
Cleanup.
2023-03-15 11:22:36 +00:00
c791be2912
Add monitor tests
...
ci/woodpecker/push/build Pipeline was successful
Details
- Add tests for monitors spanning two theories.
- Fix monitors trace update bug.
When updating a monitor trace when we define a new instance,
the monitor instance is already defined.
But we can not update the instance using the update_instance function
because this function needs a binding, i.e. a short name,
and then it will update or define a new instance if we want
to update a monitor in a super theory whose name is the same as
a monitor defined in the current theory.
Example:
in the super theory:
doc_class monitor_M =
tmM :: int
rejects "test_monitor_A"
accepts "test_monitor_head ~~ test_monitor_B ~~ test_monitor_C"
open_monitor*[test_monitor_M::monitor_M]
in the current theory:
doc_class monitor_M =
tmM :: int
rejects "test_monitor_B"
accepts "test_monitor_E ~~ test_monitor_C"
text*[test_monitor_head2::Concept_MonitorTest1.test_monitor_head]‹›
open_monitor*[test_monitor_M3::monitor_M]
...
==> ERROR : the instantiation of test_monitor_head2
will define a new instance current.test_monitor_M3
when updating the trace of super.test_monitor_M3
Hence we use the update_instance_entry function
which uses long names and only updates the entry.
2023-03-15 11:02:18 +01:00
37afd975b3
Fix thm and file anti-quotations short name bug
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-13 10:27:31 +01:00
d2a1808fa8
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
ci/woodpecker/push/build Pipeline failed
Details
2023-03-08 12:08:37 +01:00
94543a86e4
added value-assert to TestKit, improved Concept_TermAntiquotations. Still TODO's.
2023-03-08 12:08:33 +01:00
af096e56fc
value-assert-error added
2023-03-08 08:50:19 +01:00
68c1046918
Code simplification
2023-03-08 08:17:08 +01:00
Achim D. Brucker
1229db1432
Ensure that output is written within session directory.
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-06 23:23:23 +01:00
3670d30ddf
Fix declarations in traces bug
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-06 17:47:44 +01:00
542c38a89c
started revision
2023-03-06 17:13:27 +01:00
b96302f676
Add latex commands to print value_ and term_
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-06 17:12:32 +01:00
f60aebccb3
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2023-03-06 16:54:14 +01:00
224a320165
...
2023-03-06 16:53:57 +01:00
92e7ee017a
Fix display option
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-06 16:14:23 +01:00
8e4ac3f118
corrected bugs.
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-06 15:08:08 +01:00
9fae991ea0
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
ci/woodpecker/push/build Pipeline failed
Details
2023-03-06 14:00:34 +01:00
6e5fa2d91b
added tests with references from and to terms and code
2023-03-06 14:00:29 +01:00
10b90c823f
Fix declare_reference behavior
...
ci/woodpecker/push/build Pipeline failed
Details
- Fix "unchecked" text onto_class antiqutation option
- Update text-assert-error function to make meta-arguments optional
2023-03-06 12:20:58 +01:00
ef8ffda414
Refactor ML invariants checking
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-06 08:46:41 +01:00
48c6457f63
Code Cleanup.
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-04 13:58:51 +01:00
ef3eee03c9
extended testkit by declare tester, added consistency proofs for OntoMatching.
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-04 13:55:32 +01:00
280feb8653
improved testKit, finished Concept_Example_Low_Level invariant
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-04 09:57:14 +01:00
289d47ee56
Fix ML invariants bug
...
ci/woodpecker/push/build Pipeline failed
Details
- The ML invariants are not checked anymore. Fix it
2023-03-03 17:33:46 +01:00
40e7285f0a
Fix definition* test in Concept_OntoReferencing
ci/woodpecker/push/build Pipeline failed
Details
2023-03-03 11:55:02 +01:00
0f3beb846e
Further advances in a more serious test setup
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-02 18:13:15 +01:00
0f5e7f582b
LaTeX repairs
ci/woodpecker/push/build Pipeline was successful
Details
2023-03-01 23:16:38 +01:00
Burkhart Wolff
Nicolas Méric
Burkhart Wolff
Achim D. Brucker