src/Tools/isac/Isac_Mathengine.thy
branchisac-update-Isa09-2
changeset 37924 6c53fe2519e5
parent 37923 4afbcd008799
child 37925 d957275620d4
     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"