Walther Neuper <neuper@ist.tugraz.at> [Thu, 06 Jan 2011 09:02:02 +0100] rev 38087
updated course/T3_MathEngine.thy, added MAKE-ISAC-bundle
Walther Neuper <neuper@ist.tugraz.at> [Fri, 31 Dec 2010 16:10:23 +0100] rev 38086
finished course/T3_MathEngine.thy. --- moved to Download:
Isabelle2009-2-ISAC_bundle_x86-cygwin.tar.gz
Walther Neuper <neuper@ist.tugraz.at> [Fri, 31 Dec 2010 15:19:05 +0100] rev 38085
tuned
Walther Neuper <neuper@ist.tugraz.at> [Fri, 31 Dec 2010 14:58:03 +0100] rev 38084
tuned
Walther Neuper <neuper@ist.tugraz.at> [Fri, 31 Dec 2010 14:54:02 +0100] rev 38083
removed error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))
the reason was: 'TERM' and 'term' are occupied by Isabelle.
TODO: improve error diagnosis already in/near prep_ori.
Walther Neuper <neuper@ist.tugraz.at> [Thu, 30 Dec 2010 14:25:19 +0100] rev 38082
tuned
Walther Neuper <neuper@ist.tugraz.at> [Thu, 30 Dec 2010 14:24:43 +0100] rev 38081
analysed error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))
this error is caused in test/../polyminus
by wrong input data to me, autoCalculate, and NOT by bugs in me,
because me work in test/../integrate.sml and test/../diff.sml,
the latter checked in this changeset.
the error probably occurs in all expls with simplify.
Walther Neuper <neuper@ist.tugraz.at> [Wed, 29 Dec 2010 20:07:52 +0100] rev 38080
intermed. in course/T3_MathEngine.thy
two problems encountered
(1) isabelle jedit does NOT accept syntax in Test_Isac.thy,
which is accepted by isabelle emacs
Thus unnecessarily edited test/../rational.sml
(2) There is an error at Model_Problem in me poly_minus.
This will be fixed before continuing T3_MathEngine.thy
Tests are running again under isabelle emacs.
Walther Neuper <neuper@ist.tugraz.at> [Mon, 27 Dec 2010 10:38:49 +0100] rev 38079
added CTP-userinterfaces.bib
Walther Neuper <neuper@ist.tugraz.at> [Wed, 15 Dec 2010 11:05:07 +0100] rev 38078
merged