Wed, 25 Aug 2010 16:20:07 +0200renamed isac's directories and Build_Isac.thy isac-update-Isa09-2
Walther Neuper <neuper@ist.tugraz.at> [Wed, 25 Aug 2010 16:20:07 +0200] rev 37947
renamed isac's directories and Build_Isac.thy

Scripts --> ProgLang
ME --> Interpret
IsacKnowledge --> Knowledge

Wed, 25 Aug 2010 15:15:01 +0200dependencies of isac files clarified in test isac-update-Isa09-2
Walther Neuper <neuper@ist.tugraz.at> [Wed, 25 Aug 2010 15:15:01 +0200] rev 37946
dependencies of isac files clarified in test

"a --- b" means "b is dependent on a":
(dependencies between *.sml are not made explicit by Isabelle)

# library.sml, calcelems.sml, Scripts/term_G.sml --- Script.thy (see ListG.thy)
# Script.thy --- Scripts/scrtools.sml

# library.sml, calcelems.sml, Scripts/*.sml --- ME
# ME --- xmlsrc
# xmlsrc --- FE-interface

# Script.thy --- IsacKnowledge/*.thy (see IsacKnowledge/*.thy)

Tue, 24 Aug 2010 12:18:27 +0200trial on organizing dependencies, not successful isac-update-Isa09-2
Walther Neuper <neuper@ist.tugraz.at> [Tue, 24 Aug 2010 12:18:27 +0200] rev 37945
trial on organizing dependencies, not successful

Typefix.thy and Descript.thy evaluated without error,
step in Isacv_Mthengine.thy to use_thy"IsakKnowledge/Atools" hangs

Tue, 24 Aug 2010 11:46:09 +0200start of (re-?)organizing dependencies between isac's files isac-update-Isa09-2
Walther Neuper <neuper@ist.tugraz.at> [Tue, 24 Aug 2010 11:46:09 +0200] rev 37944
start of (re-?)organizing dependencies between isac's files

Current Error:
*** Theory loader: unresolved dependencies of theory "Typefix" on file(s):
"../Scripts/scrtools.sml", "../ME/mstools.sml", "../ME/ctree.sml", ....
*** At command "end" (line 43 of "/usr/local/isabisac/src/Tools/isac/IsacKnowledge/Typefix.thy")

Mon, 23 Aug 2010 17:10:57 +0200updated Typefis.thy, removed Float*, Complex* (already in Isabelle2009-2) isac-update-Isa09-2
Walther Neuper <neuper@ist.tugraz.at> [Mon, 23 Aug 2010 17:10:57 +0200] rev 37943
updated Typefis.thy, removed Float*, Complex* (already in Isabelle2009-2)

only thy-dependency to be updated in Atools.thy

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 {} \;