Walther Neuper <walther.neuper@jku.at> [Wed, 23 Sep 2020 14:54:38 +0200] rev 60063
final isabisac19 on Isabelle2019
Walther Neuper <walther.neuper@jku.at> [Tue, 22 Sep 2020 17:56:12 +0200] rev 60062
tuned
Walther Neuper <walther.neuper@jku.at> [Tue, 22 Sep 2020 17:54:56 +0200] rev 60061
tuned
Walther Neuper <walther.neuper@jku.at> [Tue, 22 Sep 2020 17:53:35 +0200] rev 60060
add Makarius' new theory_commands,
ParseC.problem works in principle (see Outer syntax errors)
Walther Neuper <walther.neuper@jku.at> [Tue, 22 Sep 2020 15:54:42 +0200] rev 60059
add Makarius' new theory_text
repair_tokens is UNFEASIBLE
Walther Neuper <walther.neuper@jku.at> [Sat, 05 Sep 2020 15:25:30 +0200] rev 60058
reset hacking Pure
Walther Neuper <walther.neuper@jku.at> [Sat, 05 Sep 2020 14:50:01 +0200] rev 60057
trial 2 including problem parser into ISAC ?Problem..?
not successful because
* repair_tokens couldn't get Position.* right
better examples required
Walther Neuper <walther.neuper@jku.at> [Wed, 02 Sep 2020 17:40:02 +0200] rev 60056
separate investigation of Outer_Syntax... to Check_Outer_Syntax.thy
Walther Neuper <walther.neuper@jku.at> [Mon, 31 Aug 2020 12:05:37 +0200] rev 60055
trial 1 including problem parser into ISAC ?Problem..?
not successful because
* Makarius' exmple ISAC deals with inner_syntax only
* Naproche parses in Haskell only.
better examples required
Walther Neuper <walther.neuper@jku.at> [Sun, 30 Aug 2020 16:21:32 +0200] rev 60054
hacking Pure (HOL fails!) to investigate handling of <> in ISAC <>
build HOL fails probably due to bufferes filled by writeln.