Walther Neuper <neuper@ist.tugraz.at> [Wed, 06 Oct 2010 14:35:43 +0200] rev 38048
rewriting in test/../integrate.sml works, too
Marco Steger <m.steger@student.tugraz.at> [Wed, 06 Oct 2010 14:39:57 +0200] rev 38047
Added working Isac-Scala-jEdit-scr!!!
Walther Neuper <neuper@ist.tugraz.at> [Tue, 05 Oct 2010 16:46:56 +0200] rev 38046
repaired 'fun calc_equ' for "op <", completed rewriting in test/../rational.sml
TODO:
# delete !theory' and repair related code (Isac.thy !)
# make_thm needs Trueprop $
# ?rename RationalI ?
Walther Neuper <neuper@ist.tugraz.at> [Tue, 05 Oct 2010 15:28:32 +0200] rev 38045
renamed "op <" to "Orderings.ord_class.less" etc
find . -type f -exec sed -i s/"\"op <\""/"\"Orderings.ord_class.less\""/g {} \;
find . -type f -exec sed -i s/"\"op <=\""/"\"Orderings.ord_class.less_eq\""/g {} \;
Walther Neuper <neuper@ist.tugraz.at> [Tue, 05 Oct 2010 14:41:16 +0200] rev 38044
intermed. test/../rational.sml, before "op *" --> "Orderings.ord_class.less"
Walther Neuper <neuper@ist.tugraz.at> [Tue, 05 Oct 2010 09:17:48 +0200] rev 38043
updated print_exn
find . -type f -exec sed -i s/"print_exn "/"OldGoals.print_exn "/g {} \;
TODO: review fun print_exn_G and handle _
Walther Neuper <neuper@ist.tugraz.at> [Tue, 05 Oct 2010 09:01:30 +0200] rev 38042
repaired assoc_thy
such that assoc_thy "Rational" works.
There are related TODOs: fun theory'2thyID, ??
Walther Neuper <neuper@ist.tugraz.at> [Tue, 05 Oct 2010 08:35:55 +0200] rev 38041
intermed. test/../rational.sml
all tests without -"- work;
interesting: theory "Rational" works, but not assoc_thy "Rational"
Walther Neuper <neuper@ist.tugraz.at> [Fri, 01 Oct 2010 18:25:06 +0200] rev 38040
all rewriting in test/../poly.sml works
Walther Neuper <neuper@ist.tugraz.at> [Fri, 01 Oct 2010 17:27:55 +0200] rev 38039
tuned: shifted last tests into respective files