1.1 --- a/test/Tools/isac/Interpret/calchead.sml Tue Jul 26 14:00:38 2011 +0200
1.2 +++ b/test/Tools/isac/Interpret/calchead.sml Tue Jul 26 14:35:06 2011 +0200
1.3 @@ -724,6 +724,3 @@
1.4 "----- WN101008 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
1.5 if nxt = ("Add_Given", Add_Given "integrateBy x") then ()
1.6 else error "clchead.sml: check specify phase step 2";
1.7 -
1.8 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.9 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
2.1 --- a/test/Tools/isac/ProgLang/calculate.sml Tue Jul 26 14:00:38 2011 +0200
2.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Tue Jul 26 14:35:06 2011 +0200
2.3 @@ -362,7 +362,7 @@
2.4 *** . Free ( aaa, real)
2.5 *** . Free ( 1, real) *)
2.6 (*===== inhibit exn AK110725 ===========================================================
2.7 - val thm = num_str real_divide_1;
2.8 + val thm = num_str @{thm real_divide_1};
2.9 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
2.10 (*val t = Free ("aaa","RealDef.real") : term*)
2.11
3.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Tue Jul 26 14:00:38 2011 +0200
3.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Tue Jul 26 14:35:06 2011 +0200
3.3 @@ -324,8 +324,6 @@
3.4 term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
3.5 (*checked visually: trace_rewrite looks like above for 2009*)
3.6
3.7 -trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
3.8 -(*show_types := false;*)
3.9 writeln "----- rewrite_ rat_mult_poly_r--------------------------";
3.10 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
3.11 (*t' = t''; (*false because of further rewrites in t'*)*)
3.12 @@ -336,36 +334,11 @@
3.13 val cond = @{term "(x / x ^^^ 2)"};
3.14 val NONE = rewrite_set_ thy true erls cond;
3.15 (* ^^^^^ goes with '====== calc. to: False' above from beginning*)
3.16 -trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
3.17 -"--------------------------------------------------------";
3.18 +
3.19
3.20 "----------- compare all prepat's existing 2010 ---------";
3.21 "----------- compare all prepat's existing 2010 ---------";
3.22 "----------- compare all prepat's existing 2010 ---------";
3.23 -(* Christian Urban, 101001
3.24 -theory Test
3.25 -imports Main Complex
3.26 -begin
3.27 -
3.28 -let
3.29 - val parser = Args.context -- Scan.lift Args.name_source
3.30 - fun term_pat (ctxt, str) = str |> ProofContext.read_term_pattern ctxt
3.31 - |> ML_Syntax.print_term |> ML_Syntax.atomic
3.32 -in
3.33 - ML_Antiquote.inline "term_pat" (parser >> term_pat)
3.34 -end
3.35 -
3.36 - val t = @{term "a + b * x = (0 ::real)"};
3.37 - val pat = @{term_pat "?l = (?r ::real)"};
3.38 - val precond = @{term_pat "is_polynomial (?l::real)"};
3.39 - val inst = Pattern.match @{theory} (pat, t) (Vartab.empty, Vartab.empty);
3.40 -
3.41 - Envir.subst_term inst precond
3.42 - |> Syntax.string_of_term @{context}
3.43 - |> writeln
3.44 -
3.45 -
3.46 -end *)
3.47 val thy = @{theory "Isac"};
3.48 val t = @{term "a + b * x = (0 ::real)"};
3.49 val pat = parse_patt thy "?l = (?r ::real)";
4.1 --- a/test/Tools/isac/ProgLang/termC.sml Tue Jul 26 14:00:38 2011 +0200
4.2 +++ b/test/Tools/isac/ProgLang/termC.sml Tue Jul 26 14:35:06 2011 +0200
4.3 @@ -204,6 +204,31 @@
4.4 parse_patt thy "?p is_addUnordered";
4.5 parse_patt thy "?p :: real";
4.6
4.7 +(* Christian Urban, 101001
4.8 +theory Test
4.9 +imports Main Complex
4.10 +begin
4.11 +
4.12 +let
4.13 + val parser = Args.context -- Scan.lift Args.name_source
4.14 + fun term_pat (ctxt, str) = str |> ProofContext.read_term_pattern ctxt
4.15 + |> ML_Syntax.print_term |> ML_Syntax.atomic
4.16 +in
4.17 + ML_Antiquote.inline "term_pat" (parser >> term_pat)
4.18 +end
4.19 +
4.20 + val t = @{term "a + b * x = (0 ::real)"};
4.21 + val pat = @{term_pat "?l = (?r ::real)"};
4.22 + val precond = @{term_pat "is_polynomial (?l::real)"};
4.23 + val inst = Pattern.match @{theory} (pat, t) (Vartab.empty, Vartab.empty);
4.24 +
4.25 + Envir.subst_term inst precond
4.26 + |> Syntax.string_of_term @{context}
4.27 + |> writeln
4.28 +
4.29 +
4.30 +end *)
4.31 +
4.32 "----------- uminus_to_string ---------------------------";
4.33 "----------- uminus_to_string ---------------------------";
4.34 "----------- uminus_to_string ---------------------------";
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/test/Tools/isac/tests-important-110722ff.txt Tue Jul 26 14:35:06 2011 +0200
5.3 @@ -0,0 +1,31 @@
5.4 +see ~/devel/isac/isac-11/
5.5 + isabisac/test/Tools/isac/
5.6 +
5.7 +110722:
5.8 +test/Tools/isac/ProgLang/termC.sml:
5.9 +"----------- subst_atomic_all ---------------------------";
5.10 +"----------- Pattern.match ------------------------------";
5.11 +
5.12 +test/Tools/isac/Knowledge/eqsystem.sml:
5.13 +"----------- refine [linear,system]-------------------------------";
5.14 +
5.15 +/usr/local/isabisac/test/Tools/isac/Knowledge/diffapp.sml
5.16 +"--------- me .. scripts for maximum-example ---------------------";
5.17 +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
5.18 +"----------- Bsp 7.27 me -----------------------------------------";
5.19 +etc
5.20 +
5.21 +/usr/local/isabisac/test/Tools/isac/Knowledge/algein.sml
5.22 +"----------- me 'Berechnung' 'erstNumerisch' ---------------------";
5.23 +"----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
5.24 +etc
5.25 +110726: mit Alexander
5.26 +ProgLang
5.27 + calculate.sml ?
5.28 + rewrite.sml ?
5.29 + termC.sml ?
5.30 + tools.sml ?
5.31 +xmlsrc
5.32 + pbl/met-hierarchies don't work
5.33 +Interpret
5.34 + max example has some errors