Mon, 23 Aug 2010 11:22:25 +0200update math-engine complete isac-update-Isa09-2
Walther Neuper <neuper@ist.tugraz.at> [Mon, 23 Aug 2010 11:22:25 +0200] rev 37942
update math-engine complete

Mon, 23 Aug 2010 11:12:59 +0200update xmlsrc/* finished isac-update-Isa09-2
Walther Neuper <neuper@ist.tugraz.at> [Mon, 23 Aug 2010 11:12:59 +0200] rev 37941
update xmlsrc/* finished

Mon, 23 Aug 2010 11:05:54 +0200updated xmlsrc/* except interface-xml.sml isac-update-Isa09-2
Walther Neuper <neuper@ist.tugraz.at> [Mon, 23 Aug 2010 11:05:54 +0200] rev 37940
updated xmlsrc/* except interface-xml.sml

thms_of --> PureThy.all_thms_of
name_of_thm --> Thm.get_name_hint

Fri, 20 Aug 2010 17:18:59 +0200finished update of all mathengine ME/* isac-update-Isa09-2
Walther Neuper <neuper@ist.tugraz.at> [Fri, 20 Aug 2010 17:18:59 +0200] rev 37939
finished update of all mathengine ME/*

Fri, 20 Aug 2010 17:02:49 +0200repaired Thm.cterm_of, string_of_cterm isac-update-Isa09-2
Walther Neuper <neuper@ist.tugraz.at> [Fri, 20 Aug 2010 17:02:49 +0200] rev 37938
repaired Thm.cterm_of, string_of_cterm

WRONG
find . -type f -exec sed -i s/"cterm_of (sign_of thy)"/"(Thm.cterm thy)"/g {} \;
CORRECTION
find . -type f -exec sed -i s/"(Thm.cterm thy)"/"(cterm_of thy)"/g {} \;
find . -type f -exec sed -i s/"Thm.cterm_of"/"cterm_of"/g {} \;
find . -type f -exec sed -i s/"string_of_cterm o (cterm_of thy)"/"Syntax.string_of_term (thy2ctxt thy)"/g {} \;

Fri, 20 Aug 2010 16:37:52 +0200updated ME/script.sml isac-update-Isa09-2
Walther Neuper <neuper@ist.tugraz.at> [Fri, 20 Aug 2010 16:37:52 +0200] rev 37937
updated ME/script.sml

found wrong replacement --> (Thm.cterm thy) in subsequent thys

Fri, 20 Aug 2010 16:21:41 +0200updated ME/appl.sml,rewtools.sml; thms_of --> PureThy.all_thms_of isac-update-Isa09-2
Walther Neuper <neuper@ist.tugraz.at> [Fri, 20 Aug 2010 16:21:41 +0200] rev 37936
updated ME/appl.sml,rewtools.sml; thms_of --> PureThy.all_thms_of

Fri, 20 Aug 2010 14:58:43 +0200pushed updates over all sml+test: isac-update-Isa09-2
Walther Neuper <neuper@ist.tugraz.at> [Fri, 20 Aug 2010 14:58:43 +0200] rev 37935
pushed updates over all sml+test:

DONE
# 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 "
TODO
# Pattern.match: only left ME/rewtools.sml, cp Scripts/term_G.sml
# there seem to be Problems with assoc_thy !?!
# a\\b --> subtract op = b a: left to indiv.files due to "grep '\\'" ?!?

Fri, 20 Aug 2010 12:25:37 +0200finished update ME/calchead.sml + pushed updates over all sml+test isac-update-Isa09-2
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 !?!

Thu, 19 Aug 2010 15:41:56 +0200sed -i s/"Sign.string_of_term (sign_of thy)"/"Syntax.string_of_term (thy2ctxt thy)" isac-update-Isa09-2
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)"