1.1 --- a/src/Tools/isac/Build_Isac.thy	Fri Aug 27 14:56:54 2010 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Mon Aug 30 14:29:49 2010 +0200
     1.3 @@ -15,11 +15,6 @@
     1.4  imports Complex_Main "ProgLang/Script" (*ListC, Tools, Script*)
     1.5  begin
     1.6  
     1.7 -ML {*
     1.8 -subtract op = [1,2,3,4,5] [4,5,6,7];
     1.9 -theory "HOL";
    1.10 -*}
    1.11 -
    1.12  ML {* 
    1.13  writeln "**** build the isac kernel = math-engine + Knowledge ***********";
    1.14  writeln "**** build the math-engine *************************************" *}
    1.15 @@ -61,12 +56,23 @@
    1.16  ML {* writeln "**** build math-engine complete **************************" *}
    1.17  
    1.18  ML {* writeln "**** build the Knowledge *********************************" *}
    1.19 -use_thy "Knowledge/Typefix"
    1.20 +(*use_thy "Knowledge/Typefix" FIXXXMEWN100827*)
    1.21  use_thy "Knowledge/Descript"
    1.22  
    1.23 -ML {*
    1.24 -111;
    1.25 -*}
    1.26 +ML {* @{thm sym} *}
    1.27 +ML {* @{thm } RS @{thm } *}
    1.28 +
    1.29 +ML {*"--------------------------------------------"*}
    1.30 +
    1.31 +
    1.32 +ML {*"--------------------------------------------"*}
    1.33 +
    1.34 +ML {* @{thm } *}
    1.35 +
    1.36 +lemma foo: 
    1.37 +by (rule )
    1.38 +
    1.39 +ML {* @{thm foo} *}
    1.40  
    1.41  (*
    1.42  use_thy "Knowledge/Atools"

     2.1 --- a/src/Tools/isac/Knowledge/Atools.thy	Fri Aug 27 14:56:54 2010 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Atools.thy	Mon Aug 30 14:29:49 2010 +0200
     2.3 @@ -6,12 +6,7 @@
     2.4          10        20        30        40        50        60        70        80
     2.5  *)
     2.6  
     2.7 -theory Atools imports Descript Typefix (*...WOULD BE REQUIRED*)
     2.8 -(*theory Atools imports Complex_Main*)
     2.9 -(*theory Atools imports "../Knowledge/Descript" "../Knowledge/Typefix" begin*)
    2.10 -uses ("../ProgLang/term.sml")
    2.11 -begin
    2.12 -use "../ProgLang/term.sml"
    2.13 +theory Atools imports Descript begin
    2.14  
    2.15  consts
    2.16  
    2.17 @@ -542,8 +537,8 @@
    2.18         
    2.19  		Calc ("Tools.Vars",eval_var "#Vars_"),
    2.20  		
    2.21 -		Thm ("if_True",num_str if_True),
    2.22 -		Thm ("if_False",num_str if_False)
    2.23 +		Thm ("if_True",num_str @{thm HOL.if_True}),
    2.24 +		Thm ("if_False",num_str @{thm HOL.if_False})
    2.25  		];
    2.26  
    2.27  ruleset' := overwritelthy thy (!ruleset',

     3.1 --- a/src/Tools/isac/Knowledge/Typefix.thy	Fri Aug 27 14:56:54 2010 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Typefix.thy	Mon Aug 30 14:29:49 2010 +0200
     3.3 @@ -2,6 +2,9 @@
     3.4     Author: Walther Neuper, hints from Makarius Wenzel
     3.5     9911xx 
     3.6     (c) due to copyright terms
     3.7 +
     3.8 +   FIXXXMEWN100827 Typefix.thy dropped;
     3.9 +                   probably without consequences, see fun typ_a2real
    3.10   *)
    3.11  
    3.12  theory Typefix imports "../ProgLang/Script" begin