src/Tools/isac/Build_Isac.thy
branchisac-update-Isa09-2
changeset 38007 d679c1f837a7
parent 38006 16d56796f5a0
child 38008 79b6cbd02681
equal deleted inserted replaced
38006:16d56796f5a0 38007:d679c1f837a7
    55 
    55 
    56 use "print_exn_G.sml"
    56 use "print_exn_G.sml"
    57 ML {* writeln "**** build math-engine complete **************************" *}
    57 ML {* writeln "**** build math-engine complete **************************" *}
    58 
    58 
    59 ML {* writeln "**** build the Knowledge *********************************" *}
    59 ML {* writeln "**** build the Knowledge *********************************" *}
    60 (**)
    60 (*use_thy "Knowledge/Delete"
    61 use_thy "Knowledge/Delete"
       
    62   use_thy "Knowledge/Descript"
    61   use_thy "Knowledge/Descript"
    63   use_thy "Knowledge/Atools"
    62   use_thy "Knowledge/Atools"
    64   use_thy "Knowledge/Simplify"
    63   use_thy "Knowledge/Simplify"
    65   use_thy "Knowledge/Poly"
    64   use_thy "Knowledge/Poly"
    66 
       
    67 ML {*
       
    68 val m = (1,[2]);
       
    69 #1 m;
       
    70 fst m;
       
    71 *}
       
    72   use_thy "Knowledge/Rational"
    65   use_thy "Knowledge/Rational"
    73   use_thy "Knowledge/PolyMinus"
    66   use_thy "Knowledge/PolyMinus"
    74   use_thy "Knowledge/Equation"
    67   use_thy "Knowledge/Equation"
    75   use_thy "Knowledge/LinEq"
    68   use_thy "Knowledge/LinEq"
    76   use_thy "Knowledge/Root"
    69   use_thy "Knowledge/Root"
    87   use_thy "Knowledge/DiffApp"
    80   use_thy "Knowledge/DiffApp"
    88   use_thy "Knowledge/Integrate"
    81   use_thy "Knowledge/Integrate"
    89   use_thy "Knowledge/EqSystem"
    82   use_thy "Knowledge/EqSystem"
    90   use_thy "Knowledge/Biegelinie"
    83   use_thy "Knowledge/Biegelinie"
    91   use_thy "Knowledge/AlgEin"
    84   use_thy "Knowledge/AlgEin"
    92  use_thy "Knowledge/Test"
    85   use_thy "Knowledge/Test"
    93 
    86 *)
    94 ML {* 111;
       
    95 *}
       
    96 
       
    97 use_thy "Knowledge/Isac"
    87 use_thy "Knowledge/Isac"
    98 
    88 
    99 
       
   100 text {*------------------------------------------*}
       
   101 (*
       
   102 *)
       
   103 end
    89 end
   104 
    90