Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity
1,495 Commits 15 Branches 10 Tags 77 MiB
Commit Graph

1495 Commits

Author SHA1 Message Date
Burkhart Wolff 466552a3d7 - debugging calculations for mutated text items 
- cleanup
- a wee bit serious testing in Attributes.thy
  of this feature.
 2018-08-24 21:57:16 +02:00
Burkhart Wolff 0f36e8b761 Milestone reached: 
- further debugging
- all tests checked
- all examples running (after updates to current attribute conventions)
 2018-08-24 17:14:39 +02:00
Burkhart Wolff cedac17646 First reasonably well-tested version with 
- access of attributes for objects created over multiple
  inheritance
- taking updates into account
 2018-08-24 16:58:06 +02:00
Burkhart Wolff 25bcc030b4 Integrated new attribute calculation machinery. 
Sort of works, but problems with inheritance.
Downward incompatibility:
only either long-names or short names allowed for attributes,
but nothing in between.
 2018-08-24 15:49:13 +02:00
Burkhart Wolff d04e09e24e Solved type instantiation problem of future common value computation alg. 
Commented il slow-motion in MyCommentedIsabelle.
 2018-08-23 11:46:20 +02:00
Burkhart Wolff 8fcc67978c Resolved the type inference riddle and worked out 
a solution (type matching and instantiation.)
Documented the interface to the type interface
in MyCommentedIsabelle with an example.
 2018-08-22 22:06:15 +02:00
Burkhart Wolff 8e09644e5c increasing robustness of generic attribute term constructor 
(adding antiquotations)
 2018-08-21 08:07:07 +02:00
Burkhart Wolff 627122c3fa New generalised attribute term constructor (untested) 
Refactoring necessary.
 2018-08-20 20:29:04 +02:00
Burkhart Wolff 5d7c32479d corrected DOF_core.get_attribute_info. 
Restructuring with this respect.
 2018-08-20 13:54:53 +02:00
Burkhart Wolff 00a4fd1c6b First attribute eval bug: 
- default terms now start from an undefined with
  correct ground type.
 2018-08-20 12:00:59 +02:00
Burkhart Wolff 4ffcf185ff Starting systematic testing and debugging of 
- default attribute construction
- attribute evaluation
 2018-08-20 11:36:04 +02:00
Burkhart Wolff 0bc3120dca Added new printing commands for doc_class and doc_item table. 2018-08-19 10:17:17 +02:00
Burkhart Wolff 7f032c439e Cleanups. 
Test environment for attribute evaluations.
 2018-08-18 14:44:39 +02:00
Burkhart Wolff b56c02cd6a Repaired bug in the meta-args parser. 
LaTeX generation for Text* environments with
antiquotation expansion works for the first time.
 2018-08-17 13:19:12 +02:00
Burkhart Wolff 1358540a62 Simplified thy_output (cleanup) and set first LaTeX meta-args generator. 
Restructuring
 2018-08-16 16:52:08 +02:00
Burkhart Wolff 0f12eb2e21 New configuration with modified Isabelle-LaTeX generator. 
Possesses Hook in order to parse meta attributes (not set so far,
default no-parse to empty string).
Current config compiles IsaDofApplications except Text*.
 2018-08-12 08:58:21 +02:00
Achim D. Brucker 5eb298b389 Added isamarkupText*-environment for development purposes. 2018-08-10 14:27:30 +02:00
Burkhart Wolff e81427061b Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF 2018-07-12 12:09:24 +01:00
Burkhart Wolff a07900bfab Some intermediate Hack to find a solution of the text* problem. 
textbis does both interactive and basically correct LaTeX generation
with antiquotation expansion.

At least a thing to study.

bu
 2018-07-12 12:08:58 +01:00
Achim D. Brucker a1a99c314a Fixed typos. 2018-07-02 22:23:05 +01:00
Burkhart Wolff 21cd7bbcfd Added some commands in preamble. 
Does not work yet.
 2018-07-02 13:06:18 +02:00
Achim D. Brucker 6a4712a9b0 Bug fix: no use of commandkey for accessing regular arguments. 2018-06-29 10:23:27 +02:00
Achim D. Brucker 86653eff41 Updated root.tex to latest version. 2018-06-29 10:21:00 +02:00
Achim D. Brucker b8d4d29ad7 Include preamble. 2018-06-29 10:18:20 +02:00
Burkhart Wolff 35a0a27c1d Kleinigkeiten. 2018-06-29 09:03:44 +02:00
Burkhart Wolff c0c92ac50c Vague pragmatics correction of the BAC example 2018-06-27 09:32:05 +02:00
Achim D. Brucker 02a697e6bb Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF 2018-06-27 09:18:44 +02:00
Achim D. Brucker bf7328c27c Added graphicx package. 2018-06-27 09:16:37 +02:00
Achim D. Brucker c857160f04 Added figure. 2018-06-27 09:13:41 +02:00
Burkhart Wolff bbf2ecb536 Kleinigkeiten um MathExam. 2018-06-27 09:12:50 +02:00
Burkhart Wolff 2ff81dbb1c Repaired MathExam 
(well, commented out offending figure* declaration leading
to bugs in Backend.)
 2018-06-26 18:50:56 +02:00
Burkhart Wolff 6277f44e75 Working on 
- the Toplevel sync problem for LaTeX output
- attribute computation
- various syntax issues
- examples.
 2018-06-26 17:40:08 +02:00
Burkhart Wolff aeb235447c Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF 2018-06-19 17:37:53 +02:00
Burkhart Wolff a0fac2d75b Configuration a la chasse du LaTeX generation bug (having its origine in the 
Isar transaction engine).
 2018-06-19 17:37:31 +02:00
Achim D. Brucker b7f2125202 Consistent use of Cartouch-delimiters. 2018-06-18 05:29:00 +01:00
Achim D. Brucker 038cd50045 Converted compactitem to itemize. 2018-06-18 05:24:01 +01:00
Achim D. Brucker 347595067f Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF 2018-06-14 22:41:22 +01:00
Achim D. Brucker f39cde669f Initial commit: CICM 2018 paper as example for the scholarly paper ontology. 2018-06-14 22:41:13 +01:00
Achim D. Brucker acbf2a52a0 Removed makeother. 2018-06-14 22:27:54 +01:00
Achim D. Brucker c78b8ba676 Removed outdated article example. 2018-06-14 22:27:21 +01:00
Achim D. Brucker f6847b4e42 Initial support for scrartcl class. 2018-06-14 22:27:01 +01:00
Burkhart Wolff bafc2405e9 this and that. 2018-06-14 15:35:14 +02:00
Achim D. Brucker edfd24aace Removed makeatother. 2018-06-13 18:20:38 +01:00
Achim D. Brucker ad37f4afb3 Added ifthen dependency. 2018-06-13 16:45:41 +01:00
Achim D. Brucker 83ac757297 Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF 2018-06-13 16:25:19 +01:00
Achim D. Brucker cae12ebaf4 Translate ~. 2018-06-13 16:25:03 +01:00
Idir AIT SADOUNE 9e6090c6a2 no message 2018-06-13 10:35:40 +02:00
Achim D. Brucker 14b7eb2a57 Removed installation instructions, as they are now in the main README.md. 2018-06-12 23:29:04 +01:00
Achim D. Brucker 03474d69ff Updated README with basic installation instructions. 2018-06-12 23:28:20 +01:00
Achim D. Brucker dfaa29734c Updated install script to support execution from top-level directory. 2018-06-12 23:20:43 +01:00