Achim D. Brucker
92f8fa5c25
Fixed naming inconsistency (cenelec vs. CENELEC_50128).
2019-07-20 22:39:06 +01:00
Achim D. Brucker
6fd22a071f
Resolved naming inconsistency (mathex_onto vs. math_exam).
2019-07-20 21:51:55 +01:00
Achim D. Brucker
8953f37629
Large directory restructuring.
...
This commit restructures the file hierarchy:
1) implementation is moved into src/ directory to clean up
the main directory and to make it easier for users to
find the README.md.
2) ontologies (both, the Isabelle-part and the LaTeX-part) are
now structured into directories.
2019-07-20 21:12:40 +01:00
Achim D. Brucker
f8013d90a2
Updated Isar notation.
2019-07-20 16:08:47 +01:00
Achim D. Brucker
e6cea1156c
Activated MathExam.
2019-07-20 15:30:13 +01:00
Achim D. Brucker
7f8ea1c115
Removed outdated BAC2017 example.
2019-07-20 15:15:04 +01:00
Achim D. Brucker
a85bcacd5b
Moved unit tests into tests directory and added test session.
2019-07-20 14:54:31 +01:00
Achim D. Brucker
189110dc0f
Cleanup.
2019-07-20 12:43:58 +01:00
Achim D. Brucker
3d01c5faf8
Cleanup.
2019-07-20 12:37:21 +01:00
Achim D. Brucker
4f911f3a23
Cleanup.
2019-07-20 12:02:05 +01:00
Achim D. Brucker
00651b385e
Cleanup.
2019-07-20 12:01:33 +01:00
Achim D. Brucker
38bd13d7d0
Cleanup.
2019-07-20 11:27:44 +01:00
Achim D. Brucker
a2d8ee9e6b
Merged the two theories for testing attribute related features.
2019-07-20 11:23:41 +01:00
Burkhart Wolff
00877b728e
regexps
2019-07-19 16:24:47 +02:00
Burkhart Wolff
e74df1be4d
doc_class syntax
2019-07-19 15:36:11 +02:00
Burkhart Wolff
44395aff2e
subsection on the HOL modeling context
2019-07-19 14:44:12 +02:00
Burkhart Wolff
6c1ed8af85
Introducing parts from SEFM, restructuring
2019-07-18 22:40:55 +02:00
Burkhart Wolff
c181c2851c
Added first somewhat realistic syntax on annotated text elements
2019-07-17 21:10:18 +02:00
Burkhart Wolff
1704c17776
New Structure discussed with adb, different shot in intro, ref to SEFM paper, first railroad dgm
2019-07-17 19:08:59 +02:00
Burkhart Wolff
a28ceb98eb
New LaTeX chapter introduced. Structuring proposal
2019-07-17 16:06:55 +02:00
Burkhart Wolff
62cf2264a2
new config of the document
2019-07-17 15:41:03 +02:00
Burkhart Wolff
67d6caf2ad
Reworked/Synced Background chapter with SEFM paper
2019-07-17 14:51:45 +02:00
Burkhart Wolff
5ff3217493
Internal Layout Polishing
2019-07-17 10:47:25 +02:00
Burkhart Wolff
869644e3b5
Proof Example
2019-07-17 10:24:41 +02:00
Burkhart Wolff
4c4194d468
Proof Example
2019-07-17 10:21:34 +02:00
Burkhart Wolff
4329bd2602
A little more explanations, more ontolgical control
2019-07-17 08:23:54 +02:00
Burkhart Wolff
58c31b59e8
completed first draft. Checks till page 47.
2019-07-16 19:33:24 +02:00
Burkhart Wolff
a7f6ab4fbd
Para on Antiquotation Registration
2019-07-16 16:40:40 +02:00
Burkhart Wolff
6f2dabbdd2
Markup section aufgeraeumt.
2019-07-15 17:56:13 +02:00
Burkhart Wolff
8acd482b96
Continued pass till pp 36.
2019-07-15 17:45:46 +02:00
Burkhart Wolff
e9a353919f
Renommage, reord of 2 snd TR report. Arrived at page 26
2019-07-15 17:14:11 +02:00
Burkhart Wolff
f2bb4f6e31
Modifications / evolutions for the second TR example.
...
Arrived at page 34.
2019-07-15 17:12:10 +02:00
Achim D. Brucker
6a1af31529
Removed relative imports in all non-trivial examples.
2019-07-12 20:20:02 +01:00
Burkhart Wolff
9c21b7a89a
restructuring intro
2019-07-12 16:32:19 +02:00
Burkhart Wolff
859e1392ec
excluding Isadof from programming manual
2019-07-12 16:17:22 +02:00
Achim D. Brucker
4ed22b6951
Added missing commands for i.e and e.g..
2019-07-02 06:15:43 +01:00
Achim D. Brucker
31e1abeaea
Port to Isabelle 2019.
2019-06-21 06:33:49 +01:00
Burkhart Wolff
30ef0c713d
merge
2019-06-20 10:31:27 +02:00
Burkhart Wolff
d74dcdf713
remerging on 2019 branch
2019-06-20 10:23:00 +02:00
Achim D. Brucker
8a8fac042e
Removed local debugging hacks that break proper build.
2019-06-17 10:07:21 +01:00
Burkhart Wolff
3b4e82b27c
New autoref - format, ...
2019-05-28 10:43:40 +02:00
Burkhart Wolff
dce560b05a
Again Unsyncref; changes in thy_output in order to tackle duplicate meta_args_problem
2019-05-28 10:18:40 +02:00
Burkhart Wolff
c4a4ca3ffc
small im[provements of comments
2019-05-27 11:58:22 +02:00
Burkhart Wolff
9e396b4778
LaTeX Generator Crash resolved, many little changes...
2019-05-27 11:03:32 +02:00
Burkhart Wolff
ed1bef5cbf
some better trace infos over the LaTeX generator Bug
2019-05-23 15:17:24 +02:00
Burkhart Wolff
803e97ce16
Experiments with the LaTeX generator
2019-05-14 09:13:42 +02:00
Burkhart Wolff
40537d4009
First Version with patched LaTeX Generator thy_output.ML
2019-04-29 22:24:32 +02:00
Burkhart Wolff
4a9e765cd3
second pass. Small errors here and there. Version in interactive mode for testing - no session Isa_DOF yet.
2019-04-29 17:32:45 +02:00
Burkhart Wolff
f89471d422
First Port of Isa_DOF to Isabelle2018 (without LaTeX Generation; Front-End Unit-Tested)
2019-04-29 17:06:03 +02:00
Achim D. Brucker
b0fbc80495
Excluded example of dangling reference from LaTex generation.
2019-04-07 17:41:41 +01:00