Burkhart Wolff
07527dbe11
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2023-03-24 17:22:49 +01:00
Burkhart Wolff
c0dc60d49e
Enlarged Free-form Section
2023-03-24 17:22:44 +01:00
Burkhart Wolff
81a50c6a9e
Reactivating failing assertions
2023-03-24 17:21:36 +01:00
Burkhart Wolff
5628eaa2dc
Code Cleanup
2023-03-24 17:20:45 +01:00
Nicolas Méric
230247de1a
Update Manual and code
...
- 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
Burkhart Wolff
0834f938a9
code cleanup
2023-03-24 12:59:54 +01:00
Burkhart Wolff
63c2acfece
improved title setup for testSuite
2023-03-24 10:41:32 +01:00
Burkhart Wolff
3a4db69184
updated Evaluation Section
2023-03-24 08:28:14 +01:00
Burkhart Wolff
3fc4688f69
updated Evaluation Section
2023-03-24 08:13:51 +01:00
Burkhart Wolff
7dbd016b5d
Pass throúgh evaluations
2023-03-24 08:08:55 +01:00
Burkhart Wolff
3b446c874d
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2023-03-21 14:33:25 +01:00
Burkhart Wolff
4de23de5ee
...
2023-03-21 14:33:21 +01:00
Nicolas Méric
4bd31be71d
Remove obsolete termrepr term anti-quotation
...
- Also some clean-up
2023-03-20 16:50:23 +01:00
Nicolas Méric
826fc489b7
Fix wrong getters and mappings naming
2023-03-17 21:09:28 +01:00
Nicolas Méric
ddcbf76353
Factorize ML invariants namespaces
2023-03-17 19:10:45 +01:00
Nicolas Méric
5ad6c0d328
Add getters and mappings for name-spaced objects
2023-03-17 14:05:05 +01:00
Nicolas Méric
34d5a194ee
Some clean-up
2023-03-16 16:31:19 +01:00
Nicolas Méric
8b09b0c135
Some clean-up
2023-03-16 16:05:46 +01:00
Achim D. Brucker
5292154687
Converted é to \'e to work around the lack of first-class unicode support.
2023-03-15 12:15:08 +00:00
Achim D. Brucker
caf966e3df
Cleanup.
2023-03-15 11:22:36 +00:00
Achim D. Brucker
6a1343fd06
Spell checking.
2023-03-15 10:52:23 +00:00
Achim D. Brucker
a7db5cc344
Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
2023-03-15 10:49:02 +00:00
Nicolas Méric
de94ef196f
Process input_term only when object_value_debug is enabled
2023-03-15 11:37:38 +01:00
Nicolas Méric
c791be2912
Add monitor tests
...
- 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
Achim D. Brucker
44528e887d
Documented limitation on using Isabelle/DOF via 'sideloading' partial sessions.
2023-03-14 23:23:23 +00:00
Achim D. Brucker
ecb1e88b78
Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
2023-03-13 13:01:07 +00:00
Achim D. Brucker
75b39bc168
Build document build engine also for main Isabelle/DOF component.
2023-03-13 13:00:49 +00:00
Nicolas Méric
dde865520a
Disable invariants checking for declare_reference* without meta args
2023-03-13 11:31:48 +01:00
Nicolas Méric
37afd975b3
Fix thm and file anti-quotations short name bug
2023-03-13 10:27:31 +01:00
Burkhart Wolff
d2a1808fa8
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2023-03-08 12:08:37 +01:00
Burkhart Wolff
94543a86e4
added value-assert to TestKit, improved Concept_TermAntiquotations. Still TODO's.
2023-03-08 12:08:33 +01:00
Burkhart Wolff
af096e56fc
value-assert-error added
2023-03-08 08:50:19 +01:00
Burkhart Wolff
68c1046918
Code simplification
2023-03-08 08:17:08 +01:00
Achim D. Brucker
1229db1432
Ensure that output is written within session directory.
2023-03-06 23:23:23 +01:00
Nicolas Méric
3670d30ddf
Fix declarations in traces bug
2023-03-06 17:47:44 +01:00
Burkhart Wolff
542c38a89c
started revision
2023-03-06 17:13:27 +01:00
Nicolas Méric
b96302f676
Add latex commands to print value_ and term_
2023-03-06 17:12:32 +01:00
Burkhart Wolff
f60aebccb3
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2023-03-06 16:54:14 +01:00
Burkhart Wolff
224a320165
...
2023-03-06 16:53:57 +01:00
Nicolas Méric
92e7ee017a
Fix display option
2023-03-06 16:14:23 +01:00
Burkhart Wolff
8e4ac3f118
corrected bugs.
2023-03-06 15:08:08 +01:00
Burkhart Wolff
9fae991ea0
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2023-03-06 14:00:34 +01:00
Burkhart Wolff
6e5fa2d91b
added tests with references from and to terms and code
2023-03-06 14:00:29 +01:00
Nicolas Méric
b1a0d5d739
Fix non unchecked text class anti-quotation
2023-03-06 13:10:20 +01:00
Nicolas Méric
10b90c823f
Fix declare_reference behavior
...
- 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
Nicolas Méric
ef8ffda414
Refactor ML invariants checking
2023-03-06 08:46:41 +01:00
Achim D. Brucker
69485fd497
Added hint on how to build the session Isabelle_DOF-Proofs.
2023-03-05 23:18:47 +00:00
Achim D. Brucker
f29d888068
Markdown cleanup.
2023-03-05 23:18:22 +00:00
Achim D. Brucker
5bf0b00fbc
Fixed string comparision for /bin/sh.
2023-03-04 19:17:05 +00:00
Achim D. Brucker
cc3e6566ca
Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
2023-03-04 14:51:56 +00:00