Walther Neuper <neuper@ist.tugraz.at> [Fri, 20 Aug 2010 12:25:37 +0200] rev 37934
finished update ME/calchead.sml + pushed updates over all sml+test
not yet tackled in upcoming files:
# ProtoPure.thy --> (theory "Pure")
# cterm_of (sign_of thy) --> (Thm.cterm thy)
# member op = --> DONE, but TODO swap args
# string_of_cterm (cterm_of (sign_of " --> "(Syntax.string_of_term (thy2ctxt "
# Pattern.match
# there seem to be Problems with assoc_thy !?!
Walther Neuper <neuper@ist.tugraz.at> [Thu, 19 Aug 2010 15:41:56 +0200] rev 37933
sed -i s/"Sign.string_of_term (sign_of thy)"/"Syntax.string_of_term (thy2ctxt thy)"
Walther Neuper <neuper@ist.tugraz.at> [Thu, 19 Aug 2010 15:36:02 +0200] rev 37932
cleanup
Walther Neuper <neuper@ist.tugraz.at> [Thu, 19 Aug 2010 15:20:53 +0200] rev 37931
Theory.theory --> theory, Library.option --> option, Some/None-->SOME/NONE in all files
Walther Neuper <neuper@ist.tugraz.at> [Thu, 19 Aug 2010 15:02:06 +0200] rev 37930
infix mem union --> member union op = ...
\\ --> subtract op = [4,5,6,7] [1,2,3,4,5] -> [1, 2, 3]
missed due to problem with grep '\\'
Walther Neuper <neuper@ist.tugraz.at> [Thu, 19 Aug 2010 12:08:42 +0200] rev 37929
reduced ctxt_Isac and ctxt_HOL to fun thy2ctxt', thy2ctxt
Walther Neuper <neuper@ist.tugraz.at> [Thu, 19 Aug 2010 12:00:46 +0200] rev 37928
updated ME/generate
Walther Neuper <neuper@ist.tugraz.at> [Wed, 18 Aug 2010 16:03:27 +0200] rev 37927
resuming after ME/ctree.sml
Walther Neuper <neuper@ist.tugraz.at> [Wed, 18 Aug 2010 13:55:23 +0200] rev 37926
replaced None-->NONE, Some-->SOME over all files
Walther Neuper <neuper@ist.tugraz.at> [Wed, 18 Aug 2010 13:53:15 +0200] rev 37925
finished ME/ctree.sml