Walther Neuper <walther.neuper@jku.at> [Tue, 17 Dec 2019 17:52:48 +0100] rev 59741
revert previous changeset, see TODO.thy
Walther Neuper <walther.neuper@jku.at> [Tue, 17 Dec 2019 17:19:34 +0100] rev 59740
shift tactic.sml after ctree.sml, leave tactic-def.sml before
note: this prepares for Tactic.applicable
Walther Neuper <walther.neuper@jku.at> [Tue, 17 Dec 2019 16:35:29 +0100] rev 59739
tuned
Walther Neuper <walther.neuper@jku.at> [Tue, 17 Dec 2019 16:33:24 +0100] rev 59738
tuned
Walther Neuper <walther.neuper@jku.at> [Tue, 17 Dec 2019 16:31:46 +0100] rev 59737
lucin: shift Istate into Interpret/ from MathEngBasic
note on previous CS: Test_Isac_Short errors from Chead.Appl --> Applicable.Appl
Walther Neuper <walther.neuper@jku.at> [Mon, 16 Dec 2019 15:56:20 +0100] rev 59736
rollback
Walther Neuper <walther.neuper@jku.at> [Mon, 16 Dec 2019 15:38:13 +0100] rev 59735
shift datatype appl: Chead --> Applicable
Walther Neuper <walther.neuper@jku.at> [Mon, 16 Dec 2019 14:03:16 +0100] rev 59734
lucin: re-build determine_next_tactic, "ONE ERROR" outcommented
note: this error has NOT been introduced by this change set, see there.
Walther Neuper <walther.neuper@jku.at> [Sat, 14 Dec 2019 13:36:40 +0100] rev 59733
remove tracing, which interfere with current investigations
Walther Neuper <walther.neuper@jku.at> [Sat, 14 Dec 2019 09:41:17 +0100] rev 59732
lucin: drop unnecessary call of determine_next_tactic