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
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