Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity
706 Commits 14 Branches 9 Tags 76 MiB
Commit Graph

19 Commits

Author SHA1 Message Date
Achim D. Brucker 6a1af31529 Removed relative imports in all non-trivial examples.
Isabelle_DOF/Isabelle_DOF/master This commit looks good Details
2019-07-12 20:20:02 +01:00
Burkhart Wolff 859e1392ec excluding Isadof from programming manual 2019-07-12 16:17:22 +02:00
Burkhart Wolff 40537d4009 First Version with patched LaTeX Generator thy_output.ML
HOL-OCL/Isabelle_DOF/Isabelle2018 There was a failure building this commit Details
2019-04-29 22:24:32 +02:00
Burkhart Wolff 4f349de9b9 some patches in install to make it run on MacOS 2019-04-06 12:08:38 +02:00
Achim D. Brucker f868d0c449 Initial setup: CENELEC 50128 example. 2019-02-05 16:30:02 +00:00
Achim D. Brucker bebf83673a Renamed CENELEC_50126 to CENELEC_50128 to match actual standard. 2019-02-05 09:42:12 +00:00
Burkhart Wolff eae495ac90 - Added monitor class-invariant for level consistency. 
- debugging here and there
- integration test
- remark : MathExam is in a pretty inconsistent state (requires discussion)
- integration test
 2018-12-18 14:29:08 +01:00
Burkhart Wolff 23bc75d08d Corrections in ontologies (revealed by examples) 
- identified problem: accept/reject conflicts were only detected at application
  time, not at declaration time :-( (leaved as "known problem" for the moment)
- new functionality for declaring doc class invariants
 2018-12-03 13:19:31 +01:00
Burkhart Wolff fe09c77b89 Moved MyCommentedIsabelle into the example/TR_my_commented isabelle 
- added build structure
- corrected LaTeX
- ... works as a first shot TR !!!
 2018-11-07 15:55:01 +01:00
Burkhart Wolff 36fac27d0c New Config for 2017 including AFP contributions for Regular-Sets and Regular Automata. 
Added a thin layer interfacing these two.
Slight textual improvements of examples (updates to more recent notations).
 2018-10-30 15:50:01 +01:00
Burkhart Wolff f1783538bd Cleanup with examples. More commendation. 
Another monitor example added (Concept_Example).
 2018-10-17 12:22:25 +02:00
Burkhart Wolff 0331c5dcbd Cleanup for the ISA infrastructure. 
Checking some Examples.
 2018-09-11 08:50:51 +02:00
Burkhart Wolff 0f36e8b761 Milestone reached: 
- further debugging
- all tests checked
- all examples running (after updates to current attribute conventions)
 2018-08-24 17:14:39 +02:00
Burkhart Wolff 25bcc030b4 Integrated new attribute calculation machinery. 
Sort of works, but problems with inheritance.
Downward incompatibility:
only either long-names or short names allowed for attributes,
but nothing in between.
 2018-08-24 15:49:13 +02:00
Burkhart Wolff 1358540a62 Simplified thy_output (cleanup) and set first LaTeX meta-args generator. 
Restructuring
 2018-08-16 16:52:08 +02:00
Burkhart Wolff 8ea00650a5 Minor corrections, refactoring, steps towards attribute calculation. 2018-04-19 11:04:11 +02:00
Burkhart Wolff 64a1c82242 Diverses 2018-04-08 11:29:59 +02:00
Burkhart Wolff 5e48dcffdf Ontology checking bug for unrelated direct sub_classes fixed. 
Enfin !
 2018-04-04 18:08:18 +02:00
Burkhart Wolff 4d09fc5e34 slight re-arrangement of the examples: 
the simple example becomes a cenelec example,
and simple got an example called Article based on
to the LNCS_onto.
 2018-04-04 16:14:37 +02:00