pierre.derathe
/
Isabelle_DOF
Archived
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
405 Commits 15 Branches 8 Tags 73 MiB
Commit Graph

168 Commits

Author SHA1 Message Date
Burkhart Wolff 8628ca81ab kleinkram 2018-11-27 11:13:49 +01: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
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
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
Burkhart Wolff 8e216c02f2 wdfs 2018-11-06 11:05:11 +01:00
Achim D. Brucker 46c51235e3 Based all examples on session 'Functional-Automata'. 2018-11-06 09:31:01 +00:00
Achim D. Brucker ab3ba421c8 Fixed ROOT (removed dependency on non-existing ontology.tex. 2018-11-06 09:30:18 +00:00
Achim D. Brucker 4aa8730762 Updated ROOT(s) setup to include AFP entries ... 2018-11-06 09:10:11 +00:00
Burkhart Wolff 9494c05593 - Improved automata-management 
- automata transformation integrated
- control option strict_checking added
- rudimentary tests in IsaDofApplications and Monitor_Example
 2018-11-05 21:42:36 +01:00
Burkhart Wolff 8d9e6cdc48 Big Bang: Restructuring the RegExp Interface, pushing it underneath Isa_DOF, factoring out example into Monitor Example. 2018-11-04 19:15:22 +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
Achim D. Brucker c7665d4dd0 Promoted sections to chapters ... 2018-10-30 01:29:53 +00:00
Achim D. Brucker 55e8f84c77 Switched to technical report. 2018-10-30 00:59:47 +00:00
Achim D. Brucker c05bedf098 Initial setup. 2018-10-30 00:58:45 +00:00
Achim D. Brucker f69d388c49 Updated template. 2018-10-30 00:52:40 +00:00
Achim D. Brucker 862d487b90 Cleanup. 2018-10-30 00:27:07 +00:00
Achim D. Brucker 2923e996f8 Minor layout fixes. 2018-10-29 23:33:21 +00:00
Burkhart Wolff 58f2bff319 no message 2018-10-17 12:31:17 +02:00
Burkhart Wolff df4cf56958 Polish 2018-10-17 12:30:11 +02: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 0de079cfbb Special ML antiquotation for the trace attribute (a cleaned up version). 2018-10-16 12:23:36 +02:00
Burkhart Wolff 93074bf24d Trace-Calculation refined. One gets the additional information WHICH oid of which class 
is added to the trace.
 2018-10-16 10:44:59 +02:00
Burkhart Wolff 50ff554d53 Typo - correction 2018-10-11 14:55:57 +02:00
Burkhart Wolff 71a889ee58 Automatic trace attribute calculation works on both Attribute and IsaDofApplications. 2018-10-11 13:38:32 +02:00
Burkhart Wolff b220233373 doc_item creation detects enabled monitors … 2018-10-09 15:56:17 +02:00
Burkhart Wolff 8b6a1af99d Kleine Reparaturen hier und da, 
IsaDofApplications Paper weiter “Markupified”.
 2018-10-09 11:59:21 +02:00
Burkhart Wolff 2c80ff8d0a Substantial progress with monitors. 
- infra-structure open_monitor_tab
- computing of enabled ness
- semantics behind open and close monitor.
 2018-10-08 15:13:47 +02:00
Burkhart Wolff 04a354f10a Diverse Code-Massagen/Restruktorationen um Monitore vorzubereiten. 2018-10-08 10:30:53 +02:00
Burkhart Wolff b1e4e64e19 Global revision of the Isa_DOF state - representation as record. 
(Since more components are to come …)
Global revision of the entire example suite.
 2018-10-05 09:45:24 +02:00
Burkhart Wolff b17110db7c comment inside meta_args problem solved. 2018-10-04 17:25:45 +02:00
Burkhart Wolff eaca1959ce Intermediate status : some spacing works. 2018-10-04 16:58:09 +02:00
Burkhart Wolff ac835ea028 First experiments with a more liberal LaTeX parser for meta-args. 2018-10-04 15:58:20 +02:00
Burkhart Wolff e4bb874d86 More markdown in the IsaDofApplications example. 
The new setup is now checked on a Mac for the first time.
 2018-10-02 10:28:24 +02:00
Achim D. Brucker 61d69394c3 Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF 2018-10-02 08:14:23 +01:00
Achim D. Brucker 30e067ec0e Added types. 2018-10-02 08:08:47 +01:00
Achim D. Brucker 484637d83c Removed Text*. 2018-10-02 00:35:50 +01:00
Achim D. Brucker 910f81768f Build script that only copies style files into generation directory. 2018-09-18 17:18:15 +01:00
Achim D. Brucker 4c9c0a2bd1 Changed type of figure width to integer. 2018-09-18 15:34:33 +01:00