Achim D. Brucker
8935d8f4e9
Improved error handling.
2019-03-30 17:18:17 +00:00
Achim D. Brucker
060dcbbabc
Introduced \isadof* command family.
2019-03-30 16:36:25 +00:00
Achim D. Brucker
13db9a9e77
Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
2019-03-25 12:23:00 +00:00
Achim D. Brucker
13b06fdce7
Added isaDof.subsection.scholarly_paper.conclusion.
2019-03-25 12:22:46 +00:00
Burkhart Wolff
ff3f2c9429
minor changes for CICM paper example.
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
2019-03-13 12:49:29 +01:00
Burkhart Wolff
7f8c77b2ef
Refactoring OntoLinkParser (for Paper)
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
2019-03-12 16:45:04 +01:00
Achim D. Brucker
b255de9ea7
Basis handling of lists in ltx_of_term.
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
2019-03-11 21:21:56 +00:00
Achim D. Brucker
d3ae88ed10
Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF
2019-03-11 20:42:51 +00:00
Burkhart Wolff
ffa44353f9
More on the small_math example used in the paper.
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
2019-03-11 09:42:49 +01:00
Achim D. Brucker
f8bcd2557c
Removed call to obsolete unquote_string.
2019-03-09 21:13:04 +00:00
Achim D. Brucker
a2a1f2dc3f
Manual merge.
2019-03-09 21:04:39 +00:00
Achim D. Brucker
a7ebfff71e
Initial implementation of ltx_of_markup.
2019-03-09 21:02:52 +00:00
Burkhart Wolff
94ade38d60
no message
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
2019-03-08 11:38:38 +01:00
Burkhart Wolff
287f8ab2a8
improved MyCommented Isa + added small onto example for CICM paper
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
2019-03-08 11:37:27 +01:00
Burkhart Wolff
7b7eeefa76
Changes on doc model.
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
2019-03-06 09:29:20 +01:00
Burkhart Wolff
d5cfaa79e8
Verschiedene Kleinigkeiten um assert*
...
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
Neuer Content in MyCommentedIsabelle: Intro FrontEnd.
2019-03-05 22:47:38 +01:00
Burkhart Wolff
67b31af3a1
Substantially improved assert* based on internal string-recoding.
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
2019-03-05 09:36:12 +01:00
Burkhart Wolff
0c7a53fe75
Minor corrections on CENELEC,
...
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
major Bug in assert* (no assert object creation on-the-fly) fixed
2019-02-27 18:42:45 +08:00
Burkhart Wolff
efe8e7c507
changed finbal state error to msg (takes into effect non-strict-checking)
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
2019-02-14 12:03:06 +01:00
Burkhart Wolff
dec5c9bf86
Many improvements on the CENELEC Onto.
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
2019-02-14 11:50:19 +01:00
Burkhart Wolff
a6c6ad7221
Towards a Consolidated CENELEC 50128.
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
2019-02-13 12:22:55 +01:00
Burkhart Wolff
5f7e7259d5
A dramatically improved ontological model of CENELEC 50128
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
2019-02-12 22:13:28 +01:00
Achim D. Brucker
eb772155ad
Changed sorry to oops to allow session build.
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
2019-02-12 01:02:28 +00:00
Burkhart Wolff
cd6e82949f
- added support for formal text statements Definition*, Lemma*, Theorem*, Conjecture*
...
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
- added lemma* theorem* corrolary* refering to Isar std commands, but ignoring the meta-args.
- Text-exercise: Improved the "Terms and Definitions" section Darstellung in der Ontologie durch
verwendung von Definition*.
2019-02-09 23:05:52 +01:00
Burkhart Wolff
65346b3f0a
kleinkram
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
2019-02-08 15:43:49 +01:00
Achim D. Brucker
8fff0730d6
Improved installation message.
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
2019-02-06 14:36:41 +00:00
Achim D. Brucker
c3ecbc8a24
Improve behaviour if md5sum is not installed.
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
2019-02-06 09:46:01 +00:00
Achim D. Brucker
04377e6727
Fixed bug causing the installation to halt during the registration of AFP entries.
2019-02-06 09:30:43 +00:00
Achim D. Brucker
0afa2ec8bb
Adding missing files for CENLEC example.
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
2019-02-05 16:32:39 +00:00
Achim D. Brucker
72510ff732
Merge.
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
2019-02-05 16:31:14 +00:00
Achim D. Brucker
f868d0c449
Initial setup: CENELEC 50128 example.
2019-02-05 16:30:02 +00:00
Achim D. Brucker
42af6b6bf9
Renamed CENELEC style to match ontology definition.
2019-02-05 15:54:28 +00:00
Burkhart Wolff
f663b7ac60
dfgdfg
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
2019-02-05 11:57:39 +01: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
0a35d3029e
iEnlever la derniere connerie
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
2019-02-04 15:15:51 +01:00
Burkhart Wolff
3d6432bfc2
correction
2019-02-04 14:50:47 +01:00
Burkhart Wolff
197f4f9cb8
This was just a little test
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
2019-02-04 14:16:09 +01:00
Burkhart Wolff
b8b5a60481
Transfer a bit more elements from CENELEC 50128 to our Ontology to get a slightly more complete vision of the thing.
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
2019-02-02 09:11:54 +01:00
Burkhart Wolff
a69b1ec2ff
More compact authoring,
...
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
eliminated {* *}
2019-01-31 10:38:18 +01:00
Burkhart Wolff
9757268b55
cleanup
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
2019-01-21 15:00:18 +01:00
Burkhart Wolff
964429368b
Repaired bug in the storage of assert* update chains.
...
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
Code could still be simplified.
unicode - inside - string problem hard since deeply intertwined in the inner-syntax parser.
better type-checking of isa terms and types.
2019-01-17 23:06:10 +01:00
Burkhart Wolff
7dfb4f2a7b
small example in ISA for properties ...
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
2019-01-17 13:31:37 +01:00
Achim D. Brucker
0c2bf6ccc4
Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
2019-01-15 19:32:53 +00:00
Achim D. Brucker
bdc7f40a5f
Avoid --output-delimiter as argument to cut.
2019-01-15 19:32:39 +00:00
Burkhart Wolff
e05041125e
lose versuch - chen.
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
2019-01-15 14:43:57 +01:00
Achim D. Brucker
26a3b37620
Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF
2019-01-11 20:54:46 +00:00
Burkhart Wolff
fbf28d4db7
improve comments for math_paper, eliminated unnecessary comments in ML
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
2019-01-11 15:01:34 +01:00
Achim D. Brucker
8aa623c857
Renamed section.
2019-01-09 22:38:14 +00:00
Achim D. Brucker
12dd12a070
Type-set keywords using a re-definable marco.
HOL-OCL/Isabelle_DOF/ci-builds This commit looks good
Details
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
2019-01-09 11:09:21 +00:00
Achim D. Brucker
60a0bbb9cb
Updated bibliographic information.
2019-01-09 10:31:51 +00:00