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
Walther Neuper <neuper@ist.tugraz.at> [Wed, 18 Aug 2010 13:40:09 +0200] rev 37924
established thy-ctxt strategy (1..2) for ME/mstools.sml
strategy in 2 steps:
(1) update isac to Isabelle2009-2 with minimal changes
(a) 'parse thy' left as is
'str2t' --> 'str2term_' according to (b)
'comp_dts thy' left as is, but returns term NOT cterm
(b) pretty printing '*2str' always without thy | ctxt
pretty printing '*2str_' always with ctxt
(2) make parsing dependent on context of calculation
(a) 'parse thy' --> 'parse ctxt' simplified by searchin 'thy'
(b) nothin to do
Walther Neuper <neuper@ist.tugraz.at> [Tue, 17 Aug 2010 09:05:51 +0200] rev 37923
cleaned Script: rules2scr_Rls, rules2scr_Seq
Walther Neuper <neuper@ist.tugraz.at> [Mon, 16 Aug 2010 16:36:19 +0200] rev 37922
changed \"plus\" -> \"PLUS\", times, power_, sqrt_, times_
with e.g find . -type f -exec sed -i s/\"divide_\"/\"DIVIDE\"/g {} \;
Respective updates in the Scripts need to be done by hand.
Walther Neuper <neuper@ist.tugraz.at> [Mon, 16 Aug 2010 16:19:53 +0200] rev 37921
finished Script/*
TODO: replace "plus" -> "PLUS", times, power_ in calclist and scripts
Marco Steger <m.steger@student.tugraz.at> [Sun, 15 Aug 2010 16:57:44 +0200] rev 37920
new branch for adapting jEdit to isac