Walther Neuper <neuper@ist.tugraz.at> [Fri, 01 Oct 2010 16:29:33 +0200] rev 38038
tuned: tests go through
Walther Neuper <neuper@ist.tugraz.at> [Fri, 01 Oct 2010 16:23:03 +0200] rev 38037
intermed. 'fun parse_patt' fixes types to real (like 'parse')
this was on the way to repair rewrite (prepat in Rrls)
Walther Neuper <neuper@ist.tugraz.at> [Fri, 01 Oct 2010 10:23:38 +0200] rev 38036
repaired 'prepat's, the patterns and preconditions for Rrls
fun parse_patt still lacks numbers_to_string, typ_a2real
because this causes a strange error in Poly.thy to be removed next
Walther Neuper <neuper@ist.tugraz.at> [Tue, 28 Sep 2010 13:30:29 +0200] rev 38035
interrupted test/../calculate.sml for 'rewrite_'
Walther Neuper <neuper@ist.tugraz.at> [Tue, 28 Sep 2010 10:10:26 +0200] rev 38034
updated "op *" --> Groups.times_class.times in src and test
find . -type f -exec sed -i s/"\"op \*\""/"\"Groups.times_class.times\""/g {} \;
Walther Neuper <neuper@ist.tugraz.at> [Tue, 28 Sep 2010 10:01:18 +0200] rev 38033
intermediate test/../calculate.sml
Walther Neuper <neuper@ist.tugraz.at> [Tue, 28 Sep 2010 09:37:41 +0200] rev 38032
replaced Some,None --> SOME,NONE in all test/../isac/*
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',