1.1 --- a/.hgignore	Fri Jul 22 12:07:01 2011 +0200
     1.2 +++ b/.hgignore	Fri Jul 22 12:10:21 2011 +0200
     1.3 @@ -39,6 +39,7 @@
     1.4  ^doc-src/.*\.snm
     1.5  ^doc-src/.*\.tex.backup
     1.6  ^doc-src/.*\.toc
     1.7 +^doc-src/.*\.ent
     1.8  ^doc-src/isac/bib*
     1.9  ^doc-src/isac/mlehnfeld/fig
    1.10  ^doc-src/isac/msteger/fig/

     2.1 --- a/doc-src/isac/jrocnik/Test_Complex.thy	Fri Jul 22 12:07:01 2011 +0200
     2.2 +++ b/doc-src/isac/jrocnik/Test_Complex.thy	Fri Jul 22 12:10:21 2011 +0200
     2.3 @@ -1,33 +1,61 @@
     2.4 -(* theory Test_Complex imports Isac begin
     2.5 -ERROR TODO                     ^^^^:
     2.6 +theory Test_Complex imports Isac begin
     2.7 +
     2.8 +section {*terms and operations*}
     2.9  ML {*
    2.10 -@{term "Complex 1 2 ^ Complex 3 4"};
    2.11 +print_depth 999; @{term "Complex 1 (2::real)"};
    2.12  *}
    2.13 -Type unification failed: Clash of types "complex" and "nat"
    2.14 -Operator:  op ^ (Complex 1 2) :: nat \<Rightarrow> complex
    2.15 -Operand:   Complex 3 4 :: complex
    2.16 -*)
    2.17 -
    2.18 -theory Test_Complex imports Main begin
    2.19 -
    2.20  ML {*
    2.21 -@{term "Complex 1 2"};
    2.22  @{term "Complex 1 2 + Complex 3 4"};
    2.23  @{term "Complex 1 2 * Complex 3 4"};
    2.24  @{term "Complex 1 2 - Complex 3 4"};
    2.25  @{term "Complex 1 2 / Complex 3 4"};
    2.26 -@{term "Complex 1 2 ^ Complex 3 4"};
    2.27 +(*@{term "Complex 1 2 ^ Complex 3 4"};
    2.28 +  Type unification failed: Clash of types "complex" and "nat"
    2.29 +  Operator:  op ^ (Complex 1 2) :: nat \<Rightarrow> complex
    2.30 +  Operand:   Complex 3 4 :: complex*)
    2.31  *}
    2.32  ML {*
    2.33 +term2str @{term "Complex 1 2 + Complex 3 4"};
    2.34 +term2str @{term "Complex 1 2 / Complex 3 4"};
    2.35 +*}
    2.36 +
    2.37 +ML {*
    2.38  val a = @{term "Complex 1 2"};
    2.39  val b = @{term "Complex 3 4"};
    2.40  (*a + (b::complex); ERROR: term + term*)
    2.41  *}
    2.42 +
    2.43 +section {*use the operations for simplification*}
    2.44 +subsection {*example 1*}
    2.45  ML {*
    2.46 -@{term "let a = Complex 1 2; b = Complex 3 4 in a + b"};
    2.47 +print_depth 1;
    2.48 +val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
    2.49  *}
    2.50  ML {*
    2.51 -(*TODO rules for simplification*)
    2.52 +val thm = @{thm "complex_add"};
    2.53 +val t = @{term "Complex 1 2 + Complex 3 4"};
    2.54 +val SOME _ = rewrite_ thy ro er true thm t;
    2.55 +val SOME (t', _) = rewrite_ thy ro er true thm t;
    2.56 +"Complex (1 + 3) (2 + 4)" = term2str t';
    2.57 +*}
    2.58 +
    2.59 +subsection {*example 2*}
    2.60 +ML {*
    2.61 +val Simplify_complex = append_rls "Simplify_complex" norm_Poly
    2.62 +  [ Thm  ("complex_add",num_str @{thm complex_add}),
    2.63 +		    Thm  ("complex_mult",num_str @{thm complex_mult})
    2.64 +		  ];
    2.65 +*}
    2.66 +ML {*
    2.67 +val t = @{term "0 * (Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))"};
    2.68 +*}
    2.69 +ML {*
    2.70 +val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
    2.71 +*}
    2.72 +ML {*
    2.73 +term2str t
    2.74 +*}
    2.75 +ML {*
    2.76  *}
    2.77  
    2.78  end

     3.1 --- a/doc-src/isac/jrocnik/Test_SUM.thy	Fri Jul 22 12:07:01 2011 +0200
     3.2 +++ b/doc-src/isac/jrocnik/Test_SUM.thy	Fri Jul 22 12:10:21 2011 +0200
     3.3 @@ -1,13 +1,7 @@
     3.4  
     3.5  theory Test_SUM imports Isac begin
     3.6  
     3.7 -ML{* writeln "**** run the test ***************************************" *}
     3.8 -
     3.9 -use"../../../test/Tools/isac/Interpret/script.sml"
    3.10 -
    3.11 -ML {*
    3.12 -@{term "(SUM i = 0..< k. f i)"}
    3.13 -*}
    3.14 +section {*trials with implicit function, probably required*}
    3.15  ML {*
    3.16  @{term "(%n :: nat. n) 2"};
    3.17  @{term "(%n. n) 2"};
    3.18 @@ -18,8 +12,11 @@
    3.19  @{term "(%n. n+n) a"};
    3.20  @{term "a+a"};
    3.21  *}
    3.22 +section {*sums*}
    3.23  ML {*
    3.24 -@{term "Integral s f k"}
    3.25 +@{term "(SUM i = 0..< k. f i)"}
    3.26 +*}
    3.27 +ML {*
    3.28  *}
    3.29  ML {*
    3.30  *}
    3.31 @@ -28,18 +25,3 @@
    3.32  
    3.33  end
    3.34  
    3.35 -
    3.36 -(*=== inhibit exn ?=============================================================
    3.37 -===== inhibit exn ?===========================================================*)
    3.38 -
    3.39 -
    3.40 -(*========== inhibit exn 110415 ================================================
    3.41 -
    3.42 -"########### testcode inserted vvv ###########################################";
    3.43 -"########### testcode inserted ^^^ ###########################################";
    3.44 -
    3.45 -============ inhibit exn 110415 ==============================================*)
    3.46 -
    3.47 -
    3.48 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    3.49 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)