Walther Neuper <wneuper@ist.tugraz.at> [Mon, 20 Apr 2015 10:33:55 +0200] rev 59110
Build_Isac.thy WORKS: shift new tests from "src" to "test"
Note: the other tests do not yet run; they will be reviewed with
"isabelle jedit -l Isac"
Walther Neuper <wneuper@ist.tugraz.at> [Mon, 20 Apr 2015 10:27:19 +0200] rev 59109
apply conversion thm <--> metaview
Note: since type thm knows the respective name,
Isac's type Thm shall be re-engineered to "Thm: thm -> rule"
together with assoc_thm, thmID_of_derivation_name', etc.
Walther Neuper <wneuper@ist.tugraz.at> [Mon, 20 Apr 2015 10:21:35 +0200] rev 59108
introduce a conversion thm <--> metaview (seen from Lucas-Interpretation)
conversion enforced by Isabelle2014 changing add_assoc --> add.assoc etc.
Walther Neuper <wneuper@ist.tugraz.at> [Tue, 14 Apr 2015 15:42:12 +0200] rev 59107
enforced add_commute --> add.commute etc breaks parse
parse @{theory} "Rewrite mult_commute False"; (*= SOME ("Rewrite mult_commute False")*)
parse @{theory} "Rewrite mult.commute False"; (*= NONE*)
Walther Neuper <wneuper@ist.tugraz.at> [Tue, 14 Apr 2015 14:36:02 +0200] rev 59106
print_depth to be replaced by configuration option "ML_print_depth"
quick-and-dirty: default_print_depth
Walther Neuper <wneuper@ist.tugraz.at> [Tue, 14 Apr 2015 13:41:48 +0200] rev 59105
build session Isac starts in Isabelle2014
however, there are error messages during build
Walther Neuper <wneuper@ist.tugraz.at> [Sat, 11 Apr 2015 11:28:31 +0200] rev 59104
merged
wenzelm [Mon, 18 Aug 2014 12:17:31 +0200] rev 59103
Added tag Isabelle2014-RC4 for changeset 113b43b84412
wenzelm [Mon, 18 Aug 2014 12:15:11 +0200] rev 59102
updated to jdk-7u67;
wenzelm [Sun, 17 Aug 2014 16:05:43 +0200] rev 59101
postpone changes in intermediate state between remove_versions/removed_versions, which is important for handle_change to refer to defined items on prover side;