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

436 Commits

Author SHA1 Message Date
Achim D. Brucker a69eceb3b4 Avoid line ending conversions for shell scripts, 2018-12-05 10:33:13 +00:00
Achim D. Brucker 781c1ed0dc Manual merge. 2018-12-04 18:15:52 +00:00
Burkhart Wolff a5f9442c6e Added global command: check_doc_global 
(* checking unresolved forward references for the moment *)
 2018-12-04 15:04:50 +01:00
Burkhart Wolff 9c8d57e573 Continuous checking of class invariants of enabled monitors. 
Regression test suite revised.
 2018-12-04 14:28:59 +01:00
Burkhart Wolff 5e7ac1c02e - Fixed the FrontEnd - level problem according to what we discussed: 
-- there are classes that do not have a level
-- title, subtitle and abstract DO NOT HAVE a level
-- text* has a level, but the level "None"

- Tested whatever we have as examples
 2018-12-04 10:41:34 +01:00
Achim D. Brucker 459538a1b7 Figure group. 2018-12-04 06:05:49 +00:00
Achim D. Brucker 0f2dc58f5a Multi-file setup. 2018-12-04 05:31:45 +00:00
Burkhart Wolff 17c66f0fea Integrated is_monitor flag for monitor class invariants. 
Makes special treatment of monitor class invariants
possible, when changes of trace are indirect...
 2018-12-03 22:36:08 +01:00
Burkhart Wolff ac1180b529 - checking class invariants 
- checking monitor class invariants
 2018-12-03 22:18:47 +01:00
Burkhart Wolff 9c0bcd86c6 rearrangement 2018-12-03 16:48:15 +01:00
Burkhart Wolff dd942cfb99 rearrangement 2018-12-03 16:46:11 +01:00
Burkhart Wolff 04f5e99e41 First running example for class invariants. 2018-12-03 16:43:27 +01:00
Burkhart Wolff 184a17f977 Refinement: class invariants now gets also the oid from its context. 2018-12-03 14:25:04 +01:00
Burkhart Wolff 6b85bd74cd Very first example of class invariant checking ... 2018-12-03 14:14:53 +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 4da4434a27 Small corrections in the ontologies. 2018-12-03 11:23:51 +01:00
Burkhart Wolff cf31ffd68b revisions of scholarly paper and report ontologies 2018-11-28 10:49:35 +01:00
Achim D. Brucker 25c295dd7f Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF 2018-11-27 14:22:19 +00:00
Achim D. Brucker 0b79c21d23 Upated title. 2018-11-27 14:18:54 +00:00
Achim D. Brucker 35c5aef204 Added generic intro text. 2018-11-27 14:11:10 +00:00
Achim D. Brucker d0d5567fc6 Restrucuring. 2018-11-27 13:51:12 +00:00
Achim D. Brucker 1f2551d683 Restrucuring. 2018-11-27 13:39:54 +00:00
Achim D. Brucker 21d51e7275 Restrucuring. 2018-11-27 13:22:31 +00:00
Achim D. Brucker 9d5bddea7c Restrucuring. 2018-11-27 13:11:54 +00:00
Achim D. Brucker b7e39f7d27 Initial commit. 2018-11-27 12:56:42 +00:00
Burkhart Wolff 3955d5d8f9 Added some elements in the TR onto: 
- optional TOC's
- front-matter
 2018-11-27 12:53:02 +01:00
Achim D. Brucker c32425a334 Added note about the state of the document. 2018-11-27 11:34:03 +00:00
Burkhart Wolff 8628ca81ab kleinkram 2018-11-27 11:13:49 +01:00
Achim D. Brucker 1fa3a531d6 Support of section_title and section_elem. 2018-11-27 09:42:30 +00:00
Achim D. Brucker bfdb5e5260 Restrucuring. 2018-11-27 09:41:04 +00:00
Achim D. Brucker eddc01e1c9 Cleanup. 2018-11-27 09:40:44 +00:00
Achim D. Brucker 0bc6f5521e Restrucuring. 2018-11-27 09:26:54 +00:00
Burkhart Wolff eea65018d1 Rearrangement of the group of TR examples. 
(following structure of math_exams)
 2018-11-21 11:15:21 +01:00
Burkhart Wolff 90f6c2d4ab - New checks for reject sets 
- basic infrastructure for class invariants
 2018-11-20 10:11:11 +01:00
Burkhart Wolff d406b3daeb implemented reject alphabets. (untested) 
slight corrections in MyCommentedIsabelle (MCI)
 2018-11-19 20:53:59 +01:00
Burkhart Wolff 0617315fb0 Small improvements on the term chapter of CommentedIsabelle 2018-11-19 11:32:22 +01:00
Burkhart Wolff f1eabf506c Changed the introduction of MyCommentedIsabelle 2018-11-15 15:20:22 +01:00
Burkhart Wolff 49d49cfcc4 New description of the goal package in the example (I had spare time in my FIIL exam). 2018-11-14 16:33:51 +01:00
Burkhart Wolff 256b2cac56 Exporting the .pdf version from the git-site: 2018-11-13 18:48:21 +01:00
Burkhart Wolff dcda1cc214 Introduced Syntax accept / reject. 
added some semantic for it (incomplete)
some elements on myCommentedIsabelle
 2018-11-13 15:19:02 +01:00
Achim D. Brucker fe17b87842 Added version check. 2018-11-08 16:04:17 +00:00
Burkhart Wolff 3a3e99ce98 Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF 2018-11-08 11:08:34 +01:00
Burkhart Wolff 027c501c0d Slight rearrangement in MyCommented. After some comments of readers. 2018-11-08 11:07:41 +01:00
Achim D. Brucker ea1480aecc Re-enabled use of side_by_side_figure. 2018-11-07 22:28:56 +00:00
Achim D. Brucker 221c7266fe Require subfloat (required for side_by_side_figure). 2018-11-07 22:16:27 +00:00
Achim D. Brucker e210e66213 Removed documentation of old Scala-setup (obsolete) and added hint for debugging LaTeX errors. 2018-11-07 22:15:55 +00:00
Burkhart Wolff dd35fa356a Added new TR for MyCommentedIsabelle; many textual corrections. 2018-11-07 22:41:11 +01:00
Burkhart Wolff 18b8e35380 This and that. 2018-11-07 22:37: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 3e6dc80445 - experiments with document ontologies 
- substantially more input on "MyCommentedIsabelle"
  (should be another TR example ? )
 2018-11-07 06:00:01 +01:00