Walther Neuper <neuper@ist.tugraz.at> [Thu, 18 Nov 2010 17:46:22 +0100] rev 38070
reactivated by 'hg up -C isac-update-Isa09-2'
Walther Neuper <neuper@ist.tugraz.at> [Thu, 18 Nov 2010 17:41:20 +0100] rev 38069
reactivated by 'hg branch --force decompose-isar'
Walther Neuper <neuper@ist.tugraz.at> [Thu, 18 Nov 2010 17:36:07 +0100] rev 38068
hg merge decompose-isar
Walther Neuper <neuper@ist.tugraz.at> [Thu, 18 Nov 2010 17:28:45 +0100] rev 38067
material for teacher course/T* started, Basics finished, Rewrite partial
working on the material suggested some changes in Isac
Walther Neuper <neuper@ist.tugraz.at> [Wed, 03 Nov 2010 11:54:53 +0100] rev 38066
----- final tests go through (test/../interface.sml)
# only 1 outcommented: *** exception TYPE raised (line 460 of "old_goals.ML")
# working with tests revealed inappropriateness of current test setup:
the output does not conform to the buffer structure (response, trace, isabelle)
# errors in test/../simplify outcommented (CAS input, input final result)
Walther Neuper <neuper@ist.tugraz.at> [Wed, 03 Nov 2010 09:45:59 +0100] rev 38065
check 'autoCalculate 1 CompleteCalc': works for test/../integrate.sml
seem to have chased a phantom, but found:
# new calcstate created very differently in
(1) me > locatetac (step here only used for next tac)
(2) autocalc > step
# DIFFERENCE (1)..(2) by encode_*, e.g. '^^^' instead '^'
# 'autoCalculate 1 (Step 1) == autocalc work, but seem to skip modelling
TODO: where do these steps come from with <Next> in the GUI ?
Walther Neuper <neuper@ist.tugraz.at> [Fri, 29 Oct 2010 16:29:39 +0200] rev 38064
finished top-down repair, now start bottom-up repair along the tests
test/../integrate.sml
shows that --- autoCalc [diff,integration] --- does not work,
although --- me method [diff,integration] --- already works.
rewriting works since 377d9061ec3e for poly, rational, integrate.
Walther Neuper <neuper@ist.tugraz.at> [Fri, 29 Oct 2010 15:54:16 +0200] rev 38063
trials on scala with inssort
Walther Neuper <neuper@ist.tugraz.at> [Thu, 28 Oct 2010 11:05:24 +0200] rev 38062
intermed. stopped repair thehier, the hierarchy of thy/thm for access by isac.
reason in tests/../rewtools.sml:
"----- FIXME: rlsthmsNOTisac DOES contain thms from isac ---"
Walther Neuper <neuper@ist.tugraz.at> [Thu, 28 Oct 2010 09:24:47 +0200] rev 38061
intermed. repair thehier, the hierarchy of thy/thm for access by isac.
Problem with Theory.thms_of dropped from 2002 to 2009.
Now used Theory.axioms_of returning terms, which will cause problems,
when isac's Knowledge will prove axioms to thms.
intermed.: PureThy.all_thms_of cannot replace Theory.thms_of,
but Thm.derivation_name contains all data required ...TODO.