nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
1,956 Commits 32 Branches 0 Tags 62 MiB
Commit Graph

97 Commits

Author SHA1 Message Date
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 5ad6c0d328 Add getters and mappings for name-spaced objects 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. 2023-03-15 12:15:08 +00:00
Achim D. Brucker caf966e3df Cleanup. 2023-03-15 11:22:36 +00: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
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 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
Burkhart Wolff 48c6457f63 Code Cleanup. 2023-03-04 13:58:51 +01:00
Burkhart Wolff ef3eee03c9 extended testkit by declare tester, added consistency proofs for OntoMatching. 2023-03-04 13:55:32 +01:00
Burkhart Wolff 280feb8653 improved testKit, finished Concept_Example_Low_Level invariant 2023-03-04 09:57:14 +01:00
Nicolas Méric 289d47ee56 Fix ML invariants bug 
- The ML invariants are not checked anymore. Fix it
 2023-03-03 17:33:46 +01:00
Nicolas Méric 40e7285f0a Fix definition* test in Concept_OntoReferencing 2023-03-03 11:55:02 +01:00
Burkhart Wolff 0f3beb846e Further advances in a more serious test setup 2023-03-02 18:13:15 +01:00
Burkhart Wolff 0f5e7f582b LaTeX repairs 2023-03-01 23:16:38 +01:00
Burkhart Wolff 0b256adee9 Bug in Test ROOT 2023-03-01 23:00:09 +01:00
Burkhart Wolff cbd197e4d8 Deeper checking in Ontological Referencing 2023-03-01 22:57:27 +01:00
Burkhart Wolff 5411aa4d6b Updating Ontological Referencing Tests 2023-03-01 22:18:48 +01:00
Burkhart Wolff 1895d3b52c Updating Ontological Referencing Tests 2023-03-01 22:17:32 +01:00
Burkhart Wolff 5bee1fee8f Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF 2023-03-01 20:48:04 +01:00
Burkhart Wolff a64fca4774 ground for revision of tests: TestKit, Conceptual, Latex-tests 2023-03-01 20:47:47 +01:00
Burkhart Wolff bf4c3d618e ground for revision of tests: TestKit, Conceptual, Latex-tests 2023-03-01 20:47:28 +01:00
Nicolas Méric 511c6369dd Fix High_Level_Syntax_Invariants unit tests 2023-03-01 12:10:47 +01:00
Achim D. Brucker a055180b72 Added PDF document generation (Fixes: #22). 2023-02-22 09:52:05 +00:00
Achim D. Brucker d1c195db26 Cleanup. 2023-02-22 07:20:30 +00:00
Achim D. Brucker d766ac22df Initial commit. 2023-02-19 18:12:14 +00:00
Achim D. Brucker ba90433700 Removed links to files outside of the current session. 2023-02-19 17:46:16 +00:00
Achim D. Brucker aaeb793a51 Moved ontologies into session Isabelle_DOF-Ontologies. 2023-02-19 16:41:16 +00:00
Achim D. Brucker 38628c37dc Integrated manual into Isabelle/DOF session. 2023-02-19 15:49:07 +00:00
Achim D. Brucker 43ccaf43f7 Refactoring of session setup. 2023-02-19 13:06:00 +00:00