1.1 --- a/src/Tools/isac/Build_Isac.thy	Wed Sep 08 16:47:22 2010 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Wed Sep 08 16:54:15 2010 +0200
     1.3 @@ -73,8 +73,12 @@
     1.4  use_thy "Knowledge/RatEq"
     1.5  use_thy "Knowledge/RootRat"
     1.6  use_thy "Knowledge/RootRatEq"
     1.7 +use_thy "Knowledge/PolyEq"
     1.8 +use_thy "Knowledge/Vect"
     1.9 +use_thy "Knowledge/Calculus"
    1.10 +use_thy "Knowledge/Trig"
    1.11  
    1.12 -use_thy "Knowledge/PolyEq"
    1.13 +use_thy "Knowledge/LogExp"
    1.14  
    1.15  ML {* 
    1.16  *}
    1.17 @@ -82,10 +86,6 @@
    1.18  
    1.19  text {*------------------------------------------*}
    1.20  (*
    1.21 -use_thy "Knowledge/Vect"
    1.22 -use_thy "Knowledge/Calculus"
    1.23 -use_thy "Knowledge/Trig"
    1.24 -use_thy "Knowledge/LogExp"
    1.25  use_thy "Knowledge/Diff"
    1.26  use_thy "Knowledge/DiffApp"
    1.27  use_thy "Knowledge/Integrate"

     2.1 --- a/src/Tools/isac/Knowledge/Calculus.thy	Wed Sep 08 16:47:22 2010 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Calculus.thy	Wed Sep 08 16:54:15 2010 +0200
     2.3 @@ -1,4 +1,3 @@
     2.4 -
     2.5 -Calculus = Real +
     2.6 +theory Calculus imports Real begin
     2.7  
     2.8  end
     2.9 \ No newline at end of file

     3.1 --- a/src/Tools/isac/Knowledge/LogExp.thy	Wed Sep 08 16:47:22 2010 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy	Wed Sep 08 16:54:15 2010 +0200
     3.3 @@ -39,7 +39,8 @@
     3.4     ],
     3.5    PolyEq_prls, SOME "solve (e_e::bool, v_v)",
     3.6    [["Equation","solve_log"]]));
     3.7 -
     3.8 +*}
     3.9 +ML {*
    3.10  (** methods **)
    3.11  store_met
    3.12   (prep_met thy "met_equ_log" [] e_metID
    3.13 @@ -54,7 +55,7 @@
    3.14      "(let e_e = ((Rewrite equality_power False) @@ " ^
    3.15      "           (Rewrite exp_invers_log False) @@ " ^
    3.16      "           (Rewrite_Set norm_Poly False)) e_e " ^
    3.17 -    " in [e_])"
    3.18 +    " in [e_e])"
    3.19     ));
    3.20  *}
    3.21  

     4.1 --- a/src/Tools/isac/Knowledge/Test.sml	Wed Sep 08 16:47:22 2010 +0200
     4.2 +++ b/src/Tools/isac/Knowledge/Test.sml	Wed Sep 08 16:54:15 2010 +0200
     4.3 @@ -12,28 +12,28 @@
     4.4  
     4.5  val ttt = (term_of o the o (parse thy))
     4.6   "Script Solve_linear (e_e::bool) (v_v::real)=             \
     4.7 - \[e_]";
     4.8 + \[e_e]";
     4.9  val ttt = (term_of o the o (parse thy))
    4.10   "Script Solve_linear (e_e::bool) (v_v::real)=             \
    4.11 - \((%e_. [e_]) e_e)";
    4.12 + \((%e_. [e_e]) e_e)";
    4.13  val ttt = (term_of o the o (parse thy))
    4.14   "Script Solve_linear (e_e::bool) (v_v::real)=             \
    4.15 - \((%e_. (let e_e = e_e in [e_])) e_e)";
    4.16 + \((%e_. (let e_e = e_e in [e_e])) e_e)";
    4.17  val ttt = (term_of o the o (parse thy))
    4.18   "Script Solve_linear (e_e::bool) (v_v::real)=             \
    4.19   \((%e_. \
    4.20   \  (let e_e = ((Rewrite_Set SqRoot_simplify False) e_e)\
    4.21 - \   in [e_]))\
    4.22 + \   in [e_e]))\
    4.23   \  e_e)";
    4.24  val ttt = (term_of o the o (parse thy))
    4.25   "Script Solve_linear (e_e::bool) (v_v::real)=             \
    4.26 - \((%ee_. (let e_e = ((Rewrite_Set SqRoot_simplify False) ee_) in [e_])) e_e)";
    4.27 + \((%ee_. (let e_e = ((Rewrite_Set SqRoot_simplify False) ee_) in [e_e])) e_e)";
    4.28  
    4.29  val ttt = (term_of o the o (parse thy))
    4.30   "Script Solve_linear (e_e::bool) (v_v::real)=             \
    4.31   \(let e_e = \
    4.32   \   (Repeat ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False)) e_e)\
    4.33 - \ in [e_])";
    4.34 + \ in [e_e])";
    4.35  (*----*)
    4.36  val ttt = (term_of o the o (parse thy))
    4.37  
    4.38 @@ -45,7 +45,7 @@
    4.39   \    ((%ee_. (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_)\
    4.40   \      e_e)\
    4.41   \    e_e)\
    4.42 - \ in [e_])";
    4.43 + \ in [e_e])";
    4.44  val ttt = (term_of o the o (parse thy))
    4.45   "Script Solve_linear (e_e::bool) (v_v::real)=             \
    4.46   \(let e_e = \
    4.47 @@ -54,7 +54,7 @@
    4.48   \        ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_))\
    4.49   \      e_e)\
    4.50   \    e_e)\
    4.51 - \ in [e_])";
    4.52 + \ in [e_e])";
    4.53  val ttt = (term_of o the o (parse thy))
    4.54   "Script Solve_linear (e_e::bool) (v_v::real)=             \
    4.55   \(let e_e = \
    4.56 @@ -64,7 +64,7 @@
    4.57   \         in ((Rewrite_Set SqRoot_simplify False) e_e)) )\
    4.58   \      e_e)\
    4.59   \    e_e)\
    4.60 - \ in [e_])";
    4.61 + \ in [e_e])";
    4.62  atomty ttt;
    4.63  atomt ttt;
    4.64  
    4.65 @@ -123,7 +123,7 @@
    4.66   \  ((Repeat\
    4.67   \    (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
    4.68   \      (Rewrite_Set SqRoot_simplify False)))) e_e)\
    4.69 - \ in [e_])";
    4.70 + \ in [e_e])";
    4.71  atomty ttt;
    4.72  
    4.73  

     5.1 --- a/src/Tools/isac/Knowledge/Trig.thy	Wed Sep 08 16:47:22 2010 +0200
     5.2 +++ b/src/Tools/isac/Knowledge/Trig.thy	Wed Sep 08 16:54:15 2010 +0200
     5.3 @@ -1,4 +1,3 @@
     5.4 -
     5.5 -Trig = Real +
     5.6 +theory Trig imports Real begin
     5.7  
     5.8  end
     5.9 \ No newline at end of file

     6.1 --- a/src/Tools/isac/Knowledge/Vect.thy	Wed Sep 08 16:47:22 2010 +0200
     6.2 +++ b/src/Tools/isac/Knowledge/Vect.thy	Wed Sep 08 16:54:15 2010 +0200
     6.3 @@ -1,3 +1,3 @@
     6.4 -Vect = Real +
     6.5 +theory Vect imports Real begin
     6.6  
     6.7  end