Walther Neuper <neuper@ist.tugraz.at> [Thu, 10 Mar 2011 15:16:13 +0100] rev 41926
intermed.update Isabelle2011:
fiddling with sudo fetch, merge, push
Walther Neuper <neuper@ist.tugraz.at> [Thu, 10 Mar 2011 15:12:55 +0100] rev 41925
intermed.update Isabelle2011: after fetch ?!?
Walther Neuper <neuper@ist.tugraz.at> [Thu, 10 Mar 2011 12:45:58 +0100] rev 41924
intermed.update Isabelle2011: HOL.Trueprop
src + test
find . -type f -exec sed -i s/"\"Trueprop\""/"\"HOL.Trueprop\""/g {} \;
Walther Neuper <neuper@ist.tugraz.at> [Fri, 04 Mar 2011 11:45:02 +0100] rev 41923
tuned
Walther Neuper <neuper@ist.tugraz.at> [Fri, 04 Mar 2011 11:43:45 +0100] rev 41922
intermed.update Isabelle2001: updated "op =", "op +"
in src/../isac, test/../isac
find . -type f -exec sed -i s/"\"op =\""/"\"HOL.eq\""/g {} \;
in test/../isac
find . -type f -exec sed -i s/"\"op +\""/"\"Groups.plus_class.plus\""/g {} \;
Walther Neuper <neuper@ist.tugraz.at> [Fri, 04 Mar 2011 11:30:37 +0100] rev 41921
intermed.update Isabelle2001: make tests work
started src/Tools/isac/Knowledge/DiophantEq.thy for ML
and found in the rewriter
r = ??.Trueprop (op = ((x + ?a = ?b) = (x = ?b - ?a)) True)
Thus make test run before.
Marco Steger <m.steger@student.tugraz.at> [Sat, 05 Mar 2011 21:57:30 +0100] rev 41920
Added Isac-Isabelle-Interface to Pure.jar
Mathias Lehnfeld <bonzai@inode.at> [Thu, 03 Mar 2011 17:37:46 +0100] rev 41919
Update to Isabelle 2011: Build_Isac works now
Mathias Lehnfeld <bonzai@inode.at> [Thu, 03 Mar 2011 16:38:59 +0100] rev 41918
intermed.update to Isabelle 2011
Mathias Lehnfeld <bonzai@inode.at> [Thu, 03 Mar 2011 15:56:46 +0100] rev 41917
syntax test for contexts