Walther Neuper <neuper@ist.tugraz.at> [Tue, 28 Sep 2010 09:06:56 +0200] rev 38031
tuned error and writeln
# raise error --> error
# writeln in atomtyp, atomty, atomt and xmlsrc
Walther Neuper <neuper@ist.tugraz.at> [Tue, 28 Sep 2010 08:58:06 +0200] rev 38030
interrupted test/../integrate.sml for calculate.
strange observation: "===== test 4" shows, that thm requires type constraint
in order to be applied;
just done for PolyEq.thy in some axioms "separate_*".
come back to that after repair of calculate.
Walther Neuper <neuper@ist.tugraz.at> [Tue, 28 Sep 2010 07:37:12 +0200] rev 38029
repaired SubProblem (Thy_,.. --> SubProblem (Thy',
Marco Steger <m.steger@student.tugraz.at> [Tue, 28 Sep 2010 13:09:19 +0200] rev 38028
changed src
Marco Steger <m.steger@student.tugraz.at> [Tue, 28 Sep 2010 13:06:26 +0200] rev 38027
changed .hgignore again
Marco Steger <m.steger@student.tugraz.at> [Tue, 28 Sep 2010 13:03:21 +0200] rev 38026
changed hgignore
Walther Neuper <neuper@ist.tugraz.at> [Tue, 28 Sep 2010 07:28:10 +0200] rev 38025
repaired fun uminus_to_string, fun rewrite_terms_
rewrite now adjusts to 2 changes from 2002 to 2009-2
(1) Pattern.match requires _Trueprop $_ pat
(2) rewrite returns assumptions without _Trueprop $_ asm
Walther Neuper <neuper@ist.tugraz.at> [Mon, 27 Sep 2010 13:35:06 +0200] rev 38024
simplified testing by src/Tools/isac/Build_Test_Isac.thy
Marco Steger <m.steger@student.tugraz.at> [Mon, 27 Sep 2010 11:15:10 +0200] rev 38023
changes in isac-src. I think there are still problems in isac.scala!
Walther Neuper <neuper@ist.tugraz.at> [Sat, 25 Sep 2010 16:49:33 +0200] rev 38022
rewrite_ returns assumptions without Trueprop (as was in Isabelle2002)
# added redirect_tracing to handle looping
# in src/../isac/* replaced all writeln with tracing
TODO: review the tracing except in ProgLang/calculate.sml, rewrite.sml
in particular in xmlsrc/*