Walther Neuper <neuper@ist.tugraz.at> [Mon, 10 Jan 2011 10:19:10 +0100] rev 38090
merged
Walther Neuper <neuper@ist.tugraz.at> [Mon, 10 Jan 2011 10:15:44 +0100] rev 38089
CTP-userinterfaces: cite, ref, paragraph
Marco Steger <m.steger@student.tugraz.at> [Sun, 09 Jan 2011 15:10:40 +0100] rev 38088
added articles
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.