1.1 --- a/src/Tools/isac/Isac_Mathengine.thy Tue Aug 17 09:05:51 2010 +0200
1.2 +++ b/src/Tools/isac/Isac_Mathengine.thy Wed Aug 18 13:40:09 2010 +0200
1.3 @@ -9,6 +9,9 @@
1.4 $ cd "/home/neuper/proto2/isac/src/sml"
1.5 $ isabelle-process HOL HOL-Isac
1.6 ML> use_thy "Isac_Mathengine";
1.7 +
1.8 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.9 + 10 20 30 40 50 60 70 80
1.10 *)
1.11
1.12 header {* Loading the isac mathengine *}
1.13 @@ -30,9 +33,16 @@
1.14 use_thy"Scripts/Script"
1.15 use "Scripts/scrtools.sml"
1.16
1.17 +ML {*
1.18 +member;
1.19 +@{term 111};
1.20 +*}
1.21 +
1.22 use "ME/mstools.sml"
1.23
1.24
1.25 +
1.26 +
1.27 (*
1.28 use "ME/ctree.sml"
1.29 use "ME/ptyps.sml"