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

709 Commits

Author SHA1 Message Date
Chantal Keller 30b3526fb2 BAC2017: more structure 2018-06-06 19:24:17 +02:00
Idir AIT SADOUNE 23db0e7568 no message 2018-06-06 12:00:22 +02:00
Chantal Keller 80f92c168c BAC2017: tried proofs 2018-06-06 08:37:06 +02:00
Chantal Keller 3b7a029d35 BAC2017: first two questions 2018-06-05 20:56:02 +02:00
Chantal Keller 49f1ed5200 BAC2017: removed errors 2018-06-05 19:20:00 +02:00
Burkhart Wolff d52c5090bd First correct attribute calculation. 2018-06-05 09:39:38 +02:00
Idir AIT SADOUNE b030859ddf no message 2018-06-04 14:46:11 +02:00
Idir AIT SADOUNE 7de68e7564 no message 2018-06-04 13:44:08 +02:00
Burkhart Wolff 37123100df Massage 2018-05-29 14:13:49 +02:00
Burkhart Wolff 1fd4f76fb3 Corrected sheet, added proof. 2018-05-29 14:03:07 +02:00
Burkhart Wolff ce17b1cf58 Repaired MathExam wrt. Ontology. 2018-05-29 12:02:13 +02:00
Burkhart Wolff 5fd6261351 Restoring git state - inconsistent for whatever reason. 2018-05-28 16:10:20 +02:00
Burkhart Wolff 0f32ddb71a Restructuring the example directory. Fixing math exa stuff. 2018-05-24 11:35:35 +02:00
Burkhart Wolff 93bad550ef Some library code for attribute accesses (not yet working) 
RegExp Expression Inner Syntax defined

RexExp Parsing activated.
 2018-05-11 15:51:26 +02:00
Burkhart Wolff 83222961a2 Weiss nicht was commit 2018-05-02 09:40:47 +02:00
Idir AIT SADOUNE 86cce02f7a no message 2018-04-30 13:13:53 +02:00
Burkhart Wolff 49e3ec81f7 Kleine Korrekturen an scholerly … 2018-04-30 10:48:14 +02:00
Burkhart Wolff 4d3371705c Typechecked , corrected and pimped up the MathExam scenario 
with solution sections and an adapted role model.
Added explanations
 2018-04-29 12:42:00 +02:00
Burkhart Wolff d9dd46f1ac Syntax for += works finally. 
Examples here and there…
 2018-04-29 11:35:24 +02:00
Burkhart Wolff 5ca263711c Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF 2018-04-29 09:55:21 +02:00
Burkhart Wolff 5ff40948af merge commit 2018-04-29 09:53:51 +02:00
Achim D. Brucker f5ef91fb72 Changed type of ORCID (non-option type, just string). 2018-04-28 21:45:02 +01:00
Achim D. Brucker b90df780fe Resolved merge conflict. 2018-04-28 17:44:06 +01:00
Achim D. Brucker 3587183a3f Renaming: keyword_list => keywordlist (to avoid LaTex special characters). 2018-04-28 17:42:16 +01:00
Burkhart Wolff be3c0fa315 worked on onto and instance of Conceptual example. 
For framework paper
 2018-04-28 15:15:25 +02:00
Burkhart Wolff 3e746a4d9d Typing works (more or less) for the value. 
Sometimes schematic variables were left-overs;
was able to suppress this type of fault by additional
annotations.
Sometimes confusion o heavily overloaded field names.
Also workaround by stronger annotations.
 2018-04-27 17:12:42 +02:00
Burkhart Wolff fb9da6784e Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF 2018-04-27 12:06:06 +02:00
Burkhart Wolff f01b36997e Version without type check and updated Article.thy 2018-04-27 12:05:22 +02:00
Idir AIT SADOUNE afc1518dde no message 2018-04-27 11:33:47 +02:00
Idir AIT SADOUNE 7a47c5702f Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF 
# Conflicts:
#	examples/simple/Article.thy
 2018-04-27 11:16:41 +02:00
Idir AIT SADOUNE 01dac36275 no message 2018-04-27 11:15:27 +02:00
Burkhart Wolff 5bcd4c19b1 Intermediate Version 
- attribute value generation
- update interpreted
- type-checking integrated but crashes
- news on scholarly_paper …
 2018-04-27 10:34:24 +02:00
Burkhart Wolff 0474c47957 Thanks to a decisive Hint by Frederic Tuong: 
Managed to solve the Top-level-transaction problem
in “enriched_document_command”. Yay !!!
 2018-04-24 21:44:28 +02:00
Burkhart Wolff b54ed35466 Polishing in 3 and 4, micro-shortening, and new stuff in 4. 2018-04-22 13:47:29 +02:00
Burkhart Wolff 8ea00650a5 Minor corrections, refactoring, steps towards attribute calculation. 2018-04-19 11:04:11 +02:00
Burkhart Wolff 066396cfae Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF 2018-04-18 14:47:12 +02:00
Burkhart Wolff 99bdf17712 parsing and internal type-checking works. 
No integral type checking yet, and no execution.
 2018-04-18 14:46:28 +02:00
Idir AIT SADOUNE 2e185d9c25 no message 2018-04-18 09:36:21 +02:00
Idir AIT SADOUNE baa3ee9b45 no message 2018-04-17 16:43:08 +02:00
Burkhart Wolff 4c7a8ed91a kleinkram 2018-04-09 11:54:54 +02:00
Burkhart Wolff 64a1c82242 Diverses 2018-04-08 11:29:59 +02:00
Idir AIT SADOUNE c3a4111833 no message 2018-04-06 14:25:21 +02:00
Idir AIT SADOUNE 376c3fdd3b no message 2018-04-06 14:13:17 +02:00
Burkhart Wolff 46e1be6411 Added syntax for update_instance*… 
+= variant does not yet work.
 2018-04-05 12:44:52 +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 027361fb03 unified syntax: 
renamed declare_reference open_monitor close_monitor
into declare_reference* open_monitor* close_monitor*
in order to simplify the task for Achim.
 2018-04-04 17:04:19 +02:00
Burkhart Wolff 229997d60a Added open/close monitor syntax. 2018-04-04 16:25:33 +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
Burkhart Wolff 5bc9ddfd52 Running Version for Antiquotqtion Generation - 
with a Big - direct sons lead to false errors
 2018-04-04 14:44:21 +02:00
Burkhart Wolff 3338fffe19 General SML code cleanup. 
Further approximation to DocRef Generation.
 2018-04-04 10:45:56 +02:00
Burkhart Wolff f3f95fe112 added syntax for modes of doc_class_references. 
For forward-references, defining references, …

Global semantics untested and undocumented -> impl paper.

Preparative step for doc_class_reference generation.
 2018-03-29 11:19:07 +02:00
Burkhart Wolff 9dfa14eaea retouches 2018-03-28 21:08:37 +02:00
Burkhart Wolff 497c79349b Slight restructuring. 
Ontology instances in one site,
separated from the Isa_DOF core.
 2018-03-21 11:59:27 +01:00
Burkhart Wolff 868e6537db Kleinkram 
- ein paar Elemente im Parser
- neue tests im Exampl
 2018-03-14 18:03:35 +01:00
Burkhart Wolff a30e2061cd A decisive intermediate step: got sub-classing running, 
and pervasive point-and-click on doc-class references.

The entire thing starts to get presentable.
 2018-02-28 14:06:52 +01:00
Burkhart Wolff 6c59d9ba15 Refined the management of document classes and doc item refs. 
Refs were internally stored as global names.
Cross-Referencing over file-boundaries seems to work.
 2018-02-27 12:02:19 +01:00
Burkhart Wolff a64ed349d9 Added more checks. 
doc_class references now consequently based on short_names (for now).
 2018-02-09 12:25:15 +01:00
Burkhart Wolff 1d8872272b Management of doc_classes added, 
elementary checking of  doc-class referencing.
 2018-02-08 16:25:15 +01:00
Burkhart Wolff e29ee3789d Kind of current status. 
Crudely carved out of an other repository - not sure that this works.
 2018-02-07 19:44:27 +01:00