# HG changeset patch # User Mathias Lehnfeld # Date 1302105662 -7200 # Node ID 2476f5f0f9ee7182ee730449e36315ed2c377f4f # Parent c1859b72ae8da6fc08215176b91ebfc9afb93f42# Parent 1d75ac127955703ee1495dc39b21b8b35e67d6bc intermed. context introduction to specification phase diff -r c1859b72ae8d -r 2476f5f0f9ee src/Tools/isac/Build_Isac.thy --- a/src/Tools/isac/Build_Isac.thy Mon Apr 04 11:05:07 2011 +0200 +++ b/src/Tools/isac/Build_Isac.thy Wed Apr 06 18:01:02 2011 +0200 @@ -30,7 +30,7 @@ "use_thy ProgLang/Tools" "use_thy ProgLang/Script" use "ProgLang/scrtools.sml" -*) "ProgLang/Language" +*) "ProgLang/ProgLang" (* use "Interpret/mstools.sml" use "Interpret/ctree.sml" @@ -74,7 +74,7 @@ ML {* check_guhs_unique := false; *} ML {* tracing "**** isac kernel = math-engine + Knowledge complete ******" *} - +ML {* @{theory "Isac"} *} end (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. diff -r c1859b72ae8d -r 2476f5f0f9ee src/Tools/isac/Build_Test_Isac.thy --- a/src/Tools/isac/Build_Test_Isac.thy Mon Apr 04 11:05:07 2011 +0200 +++ b/src/Tools/isac/Build_Test_Isac.thy Wed Apr 06 18:01:02 2011 +0200 @@ -16,7 +16,7 @@ header {* Loading the isac mathengine *} theory Build_Test_Isac -imports Complex_Main "ProgLang/Language" "Knowledge/Isac" "Test_Isac" +imports Complex_Main "ProgLang/ProgLang" "Knowledge/Isac" "Test_Isac" begin use_thy "Build_Isac" diff -r c1859b72ae8d -r 2476f5f0f9ee src/Tools/isac/Interpret/Interpret.thy --- a/src/Tools/isac/Interpret/Interpret.thy Mon Apr 04 11:05:07 2011 +0200 +++ b/src/Tools/isac/Interpret/Interpret.thy Wed Apr 06 18:01:02 2011 +0200 @@ -3,7 +3,7 @@ (c) due to copyright terms *) -theory Interpret imports Language +theory Interpret imports ProgLang uses ("mstools.sml") ("ctree.sml") ("ptyps.sml") ("generate.sml") ("calchead.sml") ("appl.sml") ("rewtools.sml") ("script.sml") ("solve.sml") ("inform.sml") ("mathengine.sml") diff -r c1859b72ae8d -r 2476f5f0f9ee src/Tools/isac/Interpret/calchead.sml --- a/src/Tools/isac/Interpret/calchead.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/src/Tools/isac/Interpret/calchead.sml Wed Apr 06 18:01:02 2011 +0200 @@ -276,7 +276,7 @@ (*.to an input (d,ts) find the according ori and insert the ts.*) (*WN.11.03: + dont take first inter<>[]*) -fun seek_oridts ctxt sel (d,ts) [] = +(*fun seek_oridts ctxt sel (d,ts) [] = ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts))) ^ "') not found in oris (typed)", (0, [], sel, d, ts) : ori, @@ -286,6 +286,21 @@ then ("", (id,vat,sel,d, inter op = ts ts'):ori, ts') + else seek_oridts ctxt sel (d,ts) oris;*) + +fun seek_oridts ctxt sel (d,ts) [] = + ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt) + (comp_dts (d,ts))) ^ + "') not found in oris (typed)", (0, [], sel, d, ts) : ori, + []) + | seek_oridts ctxt sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) = + if sel = sel' andalso d=d' andalso (inter op = ts ts') <> [] + then if sel = sel' + then ("", + (id,vat,sel,d, inter op = ts ts'):ori, + ts') + else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts))) + ^ " not for " ^ sel, e_ori_, []) else seek_oridts ctxt sel (d,ts) oris; (*.to an input (_,ts) find the according ori and insert the ts.*) diff -r c1859b72ae8d -r 2476f5f0f9ee src/Tools/isac/Knowledge/Delete.thy --- a/src/Tools/isac/Knowledge/Delete.thy Mon Apr 04 11:05:07 2011 +0200 +++ b/src/Tools/isac/Knowledge/Delete.thy Wed Apr 06 18:01:02 2011 +0200 @@ -3,7 +3,7 @@ (c) due to copyright terms *) -theory Delete imports "../ProgLang/Language" begin +theory Delete imports "../ProgLang/ProgLang" begin axioms (* theorems which are available only with long names, which can not yet be handled in isac's scripts *) diff -r c1859b72ae8d -r 2476f5f0f9ee src/Tools/isac/ProgLang/Language.thy --- a/src/Tools/isac/ProgLang/Language.thy Mon Apr 04 11:05:07 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ -(* Title: collect all defitions for the program language - Author: Walther Neuper 100831 - (c) due to copyright terms - *) - -theory Language imports Script - uses ("../ProgLang/scrtools.sml") -begin - -use "../ProgLang/scrtools.sml" - -end \ No newline at end of file diff -r c1859b72ae8d -r 2476f5f0f9ee src/Tools/isac/ProgLang/ListC.thy --- a/src/Tools/isac/ProgLang/ListC.thy Mon Apr 04 11:05:07 2011 +0200 +++ b/src/Tools/isac/ProgLang/ListC.thy Wed Apr 06 18:01:02 2011 +0200 @@ -4,9 +4,10 @@ *) theory ListC imports Complex_Main -uses ("../library.sml")("../calcelems.sml") -("termC.sml")("calculate.sml") -("rewrite.sml") +uses ("../library.sml") + ("../calcelems.sml") + ("termC.sml")("calculate.sml") + ("rewrite.sml") begin use "../library.sml" (*indent,...*) use "../calcelems.sml" (*str_of_type, Thm,...*) diff -r c1859b72ae8d -r 2476f5f0f9ee src/Tools/isac/ProgLang/ProgLang.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/ProgLang/ProgLang.thy Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,12 @@ +(* Title: collect all defitions for the program language + Author: Walther Neuper 100831 + (c) due to copyright terms + *) + +theory ProgLang imports Script + uses ("../ProgLang/scrtools.sml") +begin + +use "../ProgLang/scrtools.sml" + +end \ No newline at end of file diff -r c1859b72ae8d -r 2476f5f0f9ee src/Tools/isac/Test_Isac.thy --- a/src/Tools/isac/Test_Isac.thy Mon Apr 04 11:05:07 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,207 +0,0 @@ -(* Title: Run_Tests on isac - Author: Walther Neuper 100808 - (c) due to copyright terms - -$ cd /usr/local/isabisac/src/Tools/isac -$ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy & -$ /usr/local/isabisac/bin/isabelle emacs Test_Isac.thy & - -RESTART emacs after having created a new Isac heap with -$ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac - -12345678901234567890123456789012345678901234567890123456789012345678901234567890 - 10 20 30 40 50 60 70 80 -Keep this width during test; otherwise \n would be inserted into string- -representation of terms and thus break some tests. -*) - -theory Test_Isac imports - "Knowledge/Isac" - "../../../test/Pure/General/Basics" - "../../../test/Pure/Isar/Test_Parse_Term" (*part.*) - "../../../test/Pure/Isar/Test_Parsers" -begin - -ML{* writeln "**** run the tests **************************************" *} -ML {* Toplevel.debug := true; *} -ML {* -(* -cd "systest"; -(*+ check kbtest/diffapp.sml for additional items in met-model*) - use"root-equ.sml"; - use"script.sml"; - (* use"script_if.sml"; WN03 missing: is_rootequation_in*) - use"scriptnew.sml"; - use"subp-rooteq.sml"; - use"tacis.sml"; - use"interface-xml.sml"; - (* use"testdaten.sml"; no update after dropping 'errorBound'*) - cd "../.."; -*) -*} -ML{* writeln "**** run systests complete ******************************" *} - -use"../../../test/Tools/isac/calcelems.sml" (*complete*) - -(* -cd"smltest/Scripts"; -*) -use"../../../test/Tools/isac/ProgLang/termC.sml" (*part.*) -ML {*print_depth 90*} -use"../../../test/Tools/isac/ProgLang/calculate.sml" (*part.*) - -ML {*store_met*} - -use"../../../test/Tools/isac/ProgLang/rewrite.sml" (*GOON*) -(* - use"listg.sml"; - use"scrtools.sml"; - use"tools.sml"; - cd "../.."; -cd"smltest/ME"; -*) - -use "../../../test/Tools/isac/Interpret/mstools.sml" (*empty*) -use "../../../test/Tools/isac/Interpret/ctree.sml" (*part.*) -use "../../../test/Tools/isac/Interpret/ptyps.sml" (*TODO*) -use "../../../test/Tools/isac/Interpret/calchead.sml" (**) -use "../../../test/Tools/isac/Interpret/rewtools.sml" (**) -(* - use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *); - use"inform.sml"; -*) -ML {*print_depth 300*} -use "../../../test/Tools/isac/Interpret/mathengine.sml" (*part.+110310*) -ML {**} -(* - use"me.sml"; - cd "../.."; -cd"smltest/xmlsrc"; - use"datatypes.sml"; - use"pbl-met-hierarchy.sml"; -use"../../../test/Tools/isac/xmlsrc/thy-hierarchy.sml" (**) -*) - -use"../../../test/Tools/isac/Frontend/interface.sml" (**) -(* - cd "../.."; -*) -ML{* writeln "**** run tests on math-engine complete ******************" *} -(* -cd"smltest/IsacKnowledge"; ---below the order as in theory Isac--- - use"atools.sml"; - use"termorder.sml"; -*) -use"../../../test/Tools/isac/Knowledge/simplify.sml" (*part.*) -(* - use"poly.sml" -*) -use"../../../test/Tools/isac/Knowledge/rational.sml" (*part.*) -(* - use"equation.sml"; - use"root.sml"; -*) -ML {* - t'; -*} - -ML {* -e186a; -str2term "x ~= 0"; -*} - -use "../../../test/Tools/isac/Knowledge/inssort.sml" (*part.*) -ML {* -(* - (*use"inssort.sml"; problems with recdef in Isabelle2002*) - use"rooteq.sml"; - use"rateq.sml"; - use"rootrateq.sml"; - - use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN - ? also check others without check 'diff.behav.'*); - use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln', - for simplification search MG - erls: 98a(1) 104a(1) 104a(2) 68a *); - use"wn.sml"; - use"trig.sml"; - use"logexp.sml"; -*) -*} -ML {*print_depth 5*} -use "../../../test/Tools/isac/Knowledge/diff.sml" (* +110310*) -use "../../../test/Tools/isac/Knowledge/integrate.sml" (*complete--110310*) -(* - use"eqsystem.sml"; -*) -ML {*print_depth 5*} -use "../../../test/Tools/isac/Knowledge/polyminus.sml" (* part. *) -(* - use"vect.sml"; - use"diffapp.sml"; - use"biegelinie.sml"; - use"algein.sml"; -*) -use "../../../test/Tools/isac/Knowledge/diophanteq.sml" (**) -ML {* -print_depth 999; -nxt; -*} -use "../../../test/Tools/isac/Knowledge/isac.sml" (**) - -ML {*print_depth 999*} -ML {*map Context.theory_name isabthys*} -ML {*print_depth 5*} - -(* - cd "../.."; -*) -(* TODO -use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test" -: -*** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library" -*** Theory loader: the error(s) above occurred while examining Thy_Info.get_theory "Foo_Language" - -use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test" -*) -use "../../../test/Pure/library.sml" (**) - -ML{* writeln "**** run tests on IsacKnowledge complete ****************" *} -(* -val path = "/home/neuper/proto3/testsml2xml/"; -pbl_hierarchy2file (path ^ "pbl/"); -pbls2file (path ^ "pbl/"); -met_hierarchy2file (path ^ "met/"); -mets2file (path ^ "met/"); -thy_hierarchy2file (path ^ "thy/"); -thes2file (path ^ "thy/"); -cd"sml"; -*) -ML{* writeln "**** tested creation of xmldata *************************" *} - -ML{*states:=[]; - writeln "========================================================="; - - writeln "**** run systests complete ***************** re-organize!"; - writeln "**** run tests on math-engine complete ******************"; - writeln "**** run tests on IsacKnowledge complete ****************"; - writeln "**** build isac kernel + run tests complete *************"; - writeln "**** tested creation of xmldata *************************"; -*} - -end - -(*=== inhibit exn ?============================================================= -===== inhibit exn ?===========================================================*) - - -(*========== inhibit exn WN110319 ============================================== - -"########### testcode inserted vvv ###########################################"; -"########### testcode inserted ^^^ ###########################################"; - -============ inhibit exn WN110319 ============================================*) - - -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) diff -r c1859b72ae8d -r 2476f5f0f9ee src/Tools/isac/Test_Some.thy --- a/src/Tools/isac/Test_Some.thy Mon Apr 04 11:05:07 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ -(* Title: Run_Tests as long Isac is not available: REPLACE 'IMPORTS' - Author: Walther Neuper 101001 - (c) copyright due to lincense terms. - -$ cd /usr/local/isabisac/test/Tools/isac -$ /usr/local/isabisac/bin/isabelle emacs Test_Some.thy & -*) - -theory Test_Some imports Isac begin -(*..................................########..................................*) - -ML{* writeln "**** run the test ***************************************" *} - -ML {* -fun term2st t = Print_Mode.setmp [] (Syntax.string_of_term -(ProofContext.init_global (Thy_Info.get_theory "Rational"))) t; -(*..............................................########......................*) -*} - -use "../../../test/Tools/isac/ProgLang/calculate.sml"; -use "../../../test/Tools/isac/Interpret/mathengine.sml"; - -end - - -(*=== inhibit exn ?============================================================= -===== inhibit exn ?===========================================================*) - - -(*========== inhibit exn 110317 ================================================ - -"########### testcode inserted vvv ###########################################"; -"########### testcode inserted ^^^ ###########################################"; - -============ inhibit exn 110317 ==============================================*) - - -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/ADDTESTS/test-depend/Build_Test.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/ADDTESTS/test-depend/Build_Test.thy Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,25 @@ +(* Title: test/../test-depend/Build_Test.thy + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*) + +header {* file dependencies according to Test_Isac.thy *} + +theory Build_Test +imports Main "testdir1/testdir1" "testdirm/testdirm" +begin + + text {* jedit and emacs treat file dependencies differently. + The files in test-depend/ mimic Test_Isac.thy. + Tests are independent by all importing Main. + We have this directory/file structure: + testdir1/testdir1.thy collects all testfiles in testdir1 + testfile-1-1.sml + testfile-1-n.sml + testdirm/testdirm.thy collects all testfiles in testdirm + testfile-m-1.sml + testfile-m-n.sml + *} + ML {*"=== test-depend/Build_test.thy =================="*} + +end diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/ADDTESTS/test-depend/testdir1/testdir1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/ADDTESTS/test-depend/testdir1/testdir1.thy Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,18 @@ +(* Title: test/../test-depend/testdir1.thy + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*) + +header {* collect all testfiles in directory testdir1/ *} + +theory testdir1 +imports Main +uses ("testfile-1-1.sml")("testfile-1-n.sml") +begin + + ML {*"===== test-depend/testdir1/testdir1.thy ========="*} + use "testfile-1-1.sml" + use "testfile-1-n.sml" + +end + diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/ADDTESTS/test-depend/testdir1/testfile-1-1.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/ADDTESTS/test-depend/testdir1/testfile-1-1.sml Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,8 @@ +(* Title: test/../test-depend/testdir1/testfile-1-1.sml + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*) + +"======= test-depend/testdir1/testfile-1-1.sml ==="; +"========= content testfile-1-1.sml =============="; + diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/ADDTESTS/test-depend/testdir1/testfile-1-n.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/ADDTESTS/test-depend/testdir1/testfile-1-n.sml Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,8 @@ +(* Title: test/../test-depend/testdir1/testfile-1-n.sml + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*) + +"======= test-depend/testdir1/testfile-1-n.sml ==="; +"========= content testfile-1-n.sml =============="; + diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/ADDTESTS/test-depend/testdirm/testdirm.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/ADDTESTS/test-depend/testdirm/testdirm.thy Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,18 @@ +(* Title: test/../test-depend/testdirm/testdirm.thy + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*) + +header {* collect all testfiles in directory testdirm/ *} + +theory testdirm +imports Main +uses ("testfile-m-1.sml")("testfile-m-n.sml") +begin + + ML {*"===== test-depend/testdir1/testdir1.thy ========="*} + use "testfile-m-1.sml" + use "testfile-m-n.sml" + +end + diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/ADDTESTS/test-depend/testdirm/testfile-m-1.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/ADDTESTS/test-depend/testdirm/testfile-m-1.sml Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,8 @@ +(* Title: test/../test-depend/testdir1/testfile-m-1.sml + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*) + +"======= test-depend/testdirm/testfile-m-1.sml ==="; +"========= content testfile-m-1.sml =============="; + diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/ADDTESTS/test-depend/testdirm/testfile-m-n.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/ADDTESTS/test-depend/testdirm/testfile-m-n.sml Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,8 @@ +(* Title: test/../test-depend/testdir1/testfile-m-n.sml + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*) + +"======= test-depend/testdirm/testfile-m-n.sml ==="; +"========= content testfile-m-n.sml =============="; + diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Frontend/messages.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/Frontend/messages.sml Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,4 @@ +(* Title: test/../messages.sml + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Frontend/states.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/Frontend/states.sml Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,4 @@ +(* Title: test/../states.sml + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Interpret/appl.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/Interpret/appl.sml Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,4 @@ +(* Title: test/../appl.sml + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Interpret/ctree.sml --- a/test/Tools/isac/Interpret/ctree.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Interpret/ctree.sml Wed Apr 06 18:01:02 2011 +0200 @@ -64,17 +64,17 @@ "this build should be detailed each time a test fails later \ \i.e. all the tests should be caught here first \ \and linked with a reference to the respective test environment"; -val fmz = ["equality (x+1=(2::int))", - "solveFor (x::int)","solutions L"]; +val fmz = ["equality (x + 1 = (2::int))", + "solveFor x","solutions L"]; val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"], ["Test","squ-equ-test-subpbl1"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,(nxt,tacx),_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (* error happens here *) (* nxt = Add_Given "equality (x + 1 = 2)" (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p)); *) -val (p,_,f,nxt,_,pt) = me (nxt,tacx) p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p)); *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Interpret/generate.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/Interpret/generate.sml Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,4 @@ +(* Title: test/../generate.sml + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Interpret/mathengine.sml --- a/test/Tools/isac/Interpret/mathengine.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Interpret/mathengine.sml Wed Apr 06 18:01:02 2011 +0200 @@ -132,9 +132,9 @@ "----- appendFormula TODO: first repair error"; val cs = ((pt,p),[]); val ("ok", cs' as (_,_,(pt,p))) = step p cs; - val ifo = (* encode "4^^^2" \*) "4^2"; val encode = I; + val ifo = (* encode "4^^^2" \*) "4^2"; (* - val ("no derivation found", (_,_,(pt, p))) = inform cs' (encode ifo); + val ("no derivation found", (_,_,(pt, p))) = inform cs' ((*encode*) ifo); here ^^^^^^^^^^^^^^^^^^^^^ should be "ok" *) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/Isac.thy --- a/test/Tools/isac/Knowledge/Isac.thy Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Knowledge/Isac.thy Wed Apr 06 18:01:02 2011 +0200 @@ -6,7 +6,12 @@ 10 20 30 40 50 60 70 80 *) -theory Isac imports Complex_Main (*TODO Build_Isac*) begin +(*WN110319 theory Isac imports Complex_Main (*TODO Build_Isac*) begin*) +theory isac imports Isac +imports "Frontend/Frontend" + PolyMinus PolyEq Vect DiffApp Biegelinie AlgEin (*InsSort +*) DiophantEq Test +begin + text {* rlsthmsNOTisac from Isabelle2002-isac are all applicable to reals; the leading parts of longnames can be dropped with some exceptions. *} diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/algein.sml --- a/test/Tools/isac/Knowledge/algein.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Knowledge/algein.sml Wed Apr 06 18:01:02 2011 +0200 @@ -5,7 +5,6 @@ use"../smltest/IsacKnowledge/algein.sml"; use"algein.sml"; *) -val thy = AlgEin.thy; "-----------------------------------------------------------------"; "table of contents -----------------------------------------------"; @@ -18,6 +17,8 @@ "-----------------------------------------------------------------"; "-----------------------------------------------------------------"; +(*=== inhibit exn ?============================================================= +val thy = AlgEin.thy; (* use"../smltest/IsacKnowledge/algein.sml"; @@ -156,3 +157,4 @@ (* use"../smltest/IsacKnowledge/algein.sml"; *) +===== inhibit exn ?===========================================================*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/atools.sml --- a/test/Tools/isac/Knowledge/atools.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Knowledge/atools.sml Wed Apr 06 18:01:02 2011 +0200 @@ -7,16 +7,18 @@ use"atools.sml"; *) -"-----------------------------------------------------------------"; -"table of contents -----------------------------------------------"; -"-----------------------------------------------------------------"; -"----------- occurs_in -------------------------------------------"; -"----------- argument_of -----------------------------------------"; -"----------- sameFunId -------------------------------------------"; -"----------- filter_sameFunId ------------------------------------"; -"----------- boollist2sum ----------------------------------------"; -"-----------------------------------------------------------------"; +"--------------------------------------------------------"; +"table of contents --------------------------------------"; +"--------------------------------------------------------"; +"----------- occurs_in ----------------------------------"; +"----------- argument_of --------------------------------"; +"----------- sameFunId ----------------------------------"; +"----------- filter_sameFunId ---------------------------"; +"----------- boollist2sum -------------------------------"; +"----------- termorder (<-- termorder.sml) --------------"; +"--------------------------------------------------------"; +(*=== inhibit exn ?============================================================= val thy = Atools.thy; @@ -126,6 +128,199 @@ trace_rewrite:=false; -(* use"IsacKnowledge/Atools.ML"; - use"../smltest/IsacKnowledge/atools.sml"; - *) \ No newline at end of file +"----------- termorder (<-- termorder.sml) --------------"; +"----------- termorder (<-- termorder.sml) --------------"; +"----------- termorder (<-- termorder.sml) --------------"; + (* tests on rewrite orders + author Matthias Goldgruber 2003 + + WN0509 do not use this file anymore, since orders require thy: + do tests in the smltest/IsacKnowledge/file.sml + where file.ML defines the respective order ! + +use"../smltest/IsacKnowledge/termorder.sml"; +*) + + + (*MK die ersten Tests*) + val substa = [(e_term, (term_of o the o (parse thy)) "a")]; + val substb = [(e_term, (term_of o the o (parse thy)) "b")]; + val substx = [(e_term, (term_of o the o (parse thy)) "x")]; + + val x1 = (term_of o the o (parse thy)) "a + b + x"; + val x2 = (term_of o the o (parse thy)) "a + x + b"; + val x3 = (term_of o the o (parse thy)) "a + x + b"; + val x4 = (term_of o the o (parse thy)) "x + a + b"; + +if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then () +else error "termorder.sml diff.behav ord_make_polynomial_in #1"; + +if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then () +else error "termorder.sml diff.behav ord_make_polynomial_in #2"; + +if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then () +else error "termorder.sml diff.behav ord_make_polynomial_in #3"; + + val aa = (term_of o the o (parse thy)) "-1 * a * x"; + val bb = (term_of o the o (parse thy)) "x^^^3"; + ord_make_polynomial_in true thy substx (aa, bb); + true; (* => LESS *) + + val aa = (term_of o the o (parse thy)) "-1 * a * x"; + val bb = (term_of o the o (parse thy)) "x^^^3"; + ord_make_polynomial_in true thy substa (aa, bb); + false; (* => GREATER *) + + (*und nach dem Re-engineering der Termorders in den 'rulesets' + kannst Du die 'gr"osste' Variable frei w"ahlen: *) + val bdv= (term_of o the o (parse thy)) "bdv"; + val x = (term_of o the o (parse thy)) "x"; + val a = (term_of o the o (parse thy)) "a"; + val b = (term_of o the o (parse thy)) "b"; + val SOME (t',_) = + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2; +if term2str t' = "b + x + a" then () +else error "termorder.sml diff.behav ord_make_polynomial_in #11"; + + val NONE = + rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2; + term2str t'; + "a + x + b"; + + val SOME (t',_) = + rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2; +if term2str t' = "a + b + x" then () +else error "termorder.sml diff.behav ord_make_polynomial_in #13"; + + + + val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2"; + val ppp = (term_of o the o (parse thy)) ppp'; + val SOME (t',_) = + rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp; +(*MG 2003... + term2str t'; + "(-6) + (-5 * x + (-15 * x ^^^ 2))";*) +if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then () +else error "termorder.sml diff.behav ord_make_polynomial_in #14"; + + val SOME (t',_) = + rewrite_set_inst "Isac"false [("bdv","x")] "make_polynomial_in" ppp'; +(*MG 2003... + "(-6) + (-5 * x + (-15) * x ^^^ 2)";*) +if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then () +else error "termorder.sml diff.behav ord_make_polynomial_in #15"; + + val ttt' = "(3*x + 5)/18"; + val ttt = (term_of o the o (parse thy)) ttt'; + val SOME (uuu,_) = + rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt; +if term2str uuu = "(5 + 3 * x) / 18" then () +else error "termorder.sml diff.behav ord_make_polynomial_in #16"; + + val SOME (uuu,_) = + rewrite_set_ thy false make_polynomial ttt; +if term2str uuu = "(5 + 3 * x) / 18" then () +else error "termorder.sml diff.behav ord_make_polynomial_in #16"; + + + + +(*-----------28.2.03: war nicht upgedatet (und ausgeklammert in ROOT.ML + + (*Aufgabe zum Einstieg in die Arbeit...*) + val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0"; + (*ein 'ruleset' aus Poly.ML wird angewandt...*) + val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t; + term2str t; + "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0"; + val SOME (t,_) = + rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t; + term2str t; + "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0"; +(* bei Verwendung von "size_of-term" nach MG :*) +(*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *) + + (*wir holen 'a' wieder aus der Klammerung heraus...*) + val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t; + term2str t; + "x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0"; +(* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *) + + val SOME (t,_) = + rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t; + term2str t; + "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0"; + (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben + "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*) + + (*das rewriting l"asst sich beobachten mit + trace_rewrite:=true; + *) + + + +"------15.11.02 --------------------------"; + val t = (term_of o the o (parse thy)) "1 + a * x + b * x"; + val bdv = (term_of o the o (parse thy)) "bdv"; + val a = (term_of o the o (parse thy)) "a"; + + trace_rewrite:=true; + (* Anwenden einer Regelmenge aus Termorder.ML: *) + val SOME (t,_) = + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; + term2str t; + val SOME (t,_) = + rewrite_set_ thy false discard_parentheses t; + term2str t; +"1 + b * x + x * a"; + + val t = (term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2"; + val SOME (t,_) = + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; + term2str t; + val SOME (t,_) = + rewrite_set_ thy false discard_parentheses t; + term2str t; +"1 + (x + b * x) * a + a ^^^ 2"; + + val t = (term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2"; + val SOME (t,_) = + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; + term2str t; + val SOME (t,_) = + rewrite_set_ thy false discard_parentheses t; + term2str t; +"1 + b * a + (7 + x) * a ^^^ 2"; + +(* MG2003 + Atools.thy grundlegende Algebra + Poly.thy Polynome + Rational.thy Br"uche + Root.thy Wurzeln + RootRat.thy Wurzen + Br"uche + Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03) + + cd"knowledge"; + remove_thy"Termorder"; + use_thy"Isac"; + + get_thm Termorder.thy "bdv_n_collect"; + get_thm (theory "Isac") "bdv_n_collect"; + +*) + val t = (term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2"; + val SOME (t,_) = + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; + term2str t; + val SOME (t,_) = + rewrite_set_ thy false discard_parentheses t; + term2str t; +"(7 + x) * a ^^^ 2"; + + val t = (term_of o the o (parse Termorder.thy)) "Pi"; + + val t = (term_of o the o (parseold thy)) "7"; + +----------------------------------------------------------------------*) +===== inhibit exn ?===========================================================*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/biegelinie.sml --- a/test/Tools/isac/Knowledge/biegelinie.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Wed Apr 06 18:01:02 2011 +0200 @@ -5,7 +5,6 @@ use"../smltest/IsacKnowledge/biegelinie.sml"; use"biegelinie.sml"; *) -val thy = Biegelinie.thy; "-----------------------------------------------------------------"; "table of contents -----------------------------------------------"; @@ -26,6 +25,8 @@ "-----------------------------------------------------------------"; "-----------------------------------------------------------------"; +(*=== inhibit exn ?============================================================= +val thy = Biegelinie.thy; "----------- the rules -------------------------------------------"; "----------- the rules -------------------------------------------"; @@ -1038,3 +1039,5 @@ (*^^^ 1 / (-1 * EI) NOT distributed - ok! ^^^^^^^^^^^^^^^^^^^^^^^*) "----- functions comming from:"; + +===== inhibit exn ?===========================================================*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/calculus.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/Knowledge/calculus.sml Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,4 @@ +(* Title: test/../calculus.sml + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/delete.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/Knowledge/delete.sml Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,4 @@ +(* Title: test/../delete.sml + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/descript.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/Knowledge/descript.sml Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,4 @@ +(* Title: test/../descript.sml + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/diffapp.sml --- a/test/Tools/isac/Knowledge/diffapp.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Knowledge/diffapp.sml Wed Apr 06 18:01:02 2011 +0200 @@ -20,6 +20,7 @@ "---------------------- 2.5.03: Make_fun_by_new_variable -----------------"; +(*=== inhibit exn ?============================================================= @@ -750,3 +751,4 @@ +===== inhibit exn ?===========================================================*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/eqsystem.sml --- a/test/Tools/isac/Knowledge/eqsystem.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed Apr 06 18:01:02 2011 +0200 @@ -6,7 +6,6 @@ use"../smltest/IsacKnowledge/eqsystem.sml"; use"eqsystem.sml"; *) -val thy = EqSystem.thy; "-----------------------------------------------------------------"; "table of contents -----------------------------------------------"; @@ -31,6 +30,8 @@ "-----------------------------------------------------------------"; "-----------------------------------------------------------------"; +(*=== inhibit exn ?============================================================= +val thy = EqSystem.thy; "----------- occur_exactly_in ------------------------------------"; "----------- occur_exactly_in ------------------------------------"; @@ -1443,3 +1444,4 @@ use"../smltest/IsacKnowledge/eqsystem.sml"; use"eqsystem.sml"; *) +===== inhibit exn ?===========================================================*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/equation.sml --- a/test/Tools/isac/Knowledge/equation.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Knowledge/equation.sml Wed Apr 06 18:01:02 2011 +0200 @@ -1,12 +1,7 @@ (* tests on the equation solver - author: Walther Neuper - 070703 + author: Walther Neuper 070703 (c) due to copyright terms - -use"../smltest/IsacKnowledge/equation.sml"; -use"equation.sml"; *) -val thy = (theory "Isac"); "-----------------------------------------------------------------"; "table of contents -----------------------------------------------"; @@ -16,6 +11,8 @@ "-----------------------------------------------------------------"; "-----------------------------------------------------------------"; +(*=== inhibit exn ?============================================================= +val thy = (theory "Isac"); "----------- CAS input -------------------------------------------"; "----------- CAS input -------------------------------------------"; @@ -31,3 +28,4 @@ show_pt pt; if p = ([], Res) andalso term2str res = "[x = 1]" then () else error "equation.sml behav.changed for CAS solve (x+1=2, x))"; +===== inhibit exn ?===========================================================*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/lineq.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/Knowledge/lineq.sml Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,4 @@ +(* Title: test/../lineq.sml + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/logexp.sml --- a/test/Tools/isac/Knowledge/logexp.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Knowledge/logexp.sml Wed Apr 06 18:01:02 2011 +0200 @@ -3,7 +3,6 @@ use"../smltest/IsacKnowledge/logexp.sml"; *) -val thy = LogExp.thy; "-----------------------------------------------------------------"; "table of contents -----------------------------------------------"; "-----------------------------------------------------------------"; @@ -12,6 +11,8 @@ "-----------------------------------------------------------------"; "-----------------------------------------------------------------"; +(*=== inhibit exn ?============================================================= +val thy = LogExp.thy; "----------- setup presentation innsbruck ------------------------"; "----------- setup presentation innsbruck ------------------------"; @@ -59,3 +60,4 @@ show_pt pt; *-------------------------------------------------------------------*) +===== inhibit exn ?===========================================================*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/poly.sml --- a/test/Tools/isac/Knowledge/poly.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Knowledge/poly.sml Wed Apr 06 18:01:02 2011 +0200 @@ -29,6 +29,7 @@ "--------------------------------------------------------"; "--------------------------------------------------------"; +(*=== inhibit exn ?============================================================= "-------- check is'_polyexp is_polyexp ------------------"; "-------- check is'_polyexp is_polyexp ------------------"; @@ -557,4 +558,5 @@ val t1 = str2term "2 * b + (3 * a + 3 * b)"; val t2 = str2term "3 * a + (2 * b + 3 * b)"; +===== inhibit exn ============================================================*) ===== inhibit exn ?===========================================================*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/polyeq.sml --- a/test/Tools/isac/Knowledge/polyeq.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Knowledge/polyeq.sml Wed Apr 06 18:01:02 2011 +0200 @@ -28,6 +28,8 @@ "-----------------------------------------------------------------"; "-----------------------------------------------------------------"; +(*=== inhibit exn ?============================================================= + val c = []; "----------- tests on predicates in problems ---------------------"; @@ -1176,3 +1178,4 @@ val ((pt,p),_) = get_calc 1; show_pt pt; interSteps 1 ([1],Res) (*no Rewrite_Set...*); +===== inhibit exn ?===========================================================*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/rateq.sml --- a/test/Tools/isac/Knowledge/rateq.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Apr 06 18:01:02 2011 +0200 @@ -11,6 +11,8 @@ "---------(1/x=5) ---------------------"; "--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------"; +(*=== inhibit exn ?============================================================= + val t = (term_of o the o (parse RatEq.thy)) "(1/b+1/x=1) is_ratequation_in x"; val SOME(t_, _) = rewrite_set_ RatEq.thy false RatEq_prls t; val result = term2str t_; @@ -143,3 +145,5 @@ else error "rateq.sml: new behaviour: [x = -2, x = 10]"; "----------- rateq.sml end--------"; + +===== inhibit exn ?===========================================================*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/root.sml --- a/test/Tools/isac/Knowledge/root.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Knowledge/root.sml Wed Apr 06 18:01:02 2011 +0200 @@ -1,5 +1,15 @@ -(* testexamples for Root, radicals - *) +(* Title: testexamples for Root, radicals + Author: Walther Neuper + (c) due to copyright terms + *) +"--------------------------------------------------------"; +"table of contents --------------------------------------"; +"--------------------------------------------------------"; +"----------- TODO ---------------------------------------"; +"--------------------------------------------------------"; +"--------------------------------------------------------"; + +(*=== inhibit exn ?============================================================= val thy = Root.thy; @@ -13,3 +23,4 @@ val SOME (t',_) = rewrite_set_ thy false Root_erls t; term2str t'; if term2str t' = "0" then () else error "root.sml: diff.behav. sqrt 1"; +===== inhibit exn ?===========================================================*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/rooteq.sml --- a/test/Tools/isac/Knowledge/rooteq.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Knowledge/rooteq.sml Wed Apr 06 18:01:02 2011 +0200 @@ -14,6 +14,9 @@ "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))-----------------"; "--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------"; "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))-----------------"; +"--------------------------------------------------------"; + +(*=== inhibit exn ?============================================================= val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x"; val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; @@ -468,3 +471,4 @@ "----------- rooteq.sml end--------"; +===== inhibit exn ?===========================================================*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/rootrateq.sml --- a/test/Tools/isac/Knowledge/rootrateq.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Wed Apr 06 18:01:02 2011 +0200 @@ -2,11 +2,15 @@ use"rootrateq.sml"; *) + +"--------------------- tests on predicates -------------------------------"; +"--------------------- tests on predicates -------------------------------"; +"--------------------- tests on predicates -------------------------------"; + +(*=== inhibit exn ?============================================================= + val thy = (theory "Isac"); -"--------------------- tests on predicates -------------------------------"; -"--------------------- tests on predicates -------------------------------"; -"--------------------- tests on predicates -------------------------------"; (* Compiler.Control.Print.printDepth:=5; (*4 default*) trace_rewrite:=true; @@ -227,3 +231,4 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => () | _ => error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]"; +===== inhibit exn ?===========================================================*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/termorder.sml --- a/test/Tools/isac/Knowledge/termorder.sml Mon Apr 04 11:05:07 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,192 +0,0 @@ - (* tests on rewrite orders - author Matthias Goldgruber 2003 - - WN0509 do not use this file anymore, since orders require thy: - do tests in the smltest/IsacKnowledge/file.sml - where file.ML defines the respective order ! - -use"../smltest/IsacKnowledge/termorder.sml"; -*) - - - (*MK die ersten Tests*) - val substa = [(e_term, (term_of o the o (parse thy)) "a")]; - val substb = [(e_term, (term_of o the o (parse thy)) "b")]; - val substx = [(e_term, (term_of o the o (parse thy)) "x")]; - - val x1 = (term_of o the o (parse thy)) "a + b + x"; - val x2 = (term_of o the o (parse thy)) "a + x + b"; - val x3 = (term_of o the o (parse thy)) "a + x + b"; - val x4 = (term_of o the o (parse thy)) "x + a + b"; - -if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then () -else error "termorder.sml diff.behav ord_make_polynomial_in #1"; - -if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then () -else error "termorder.sml diff.behav ord_make_polynomial_in #2"; - -if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then () -else error "termorder.sml diff.behav ord_make_polynomial_in #3"; - - val aa = (term_of o the o (parse thy)) "-1 * a * x"; - val bb = (term_of o the o (parse thy)) "x^^^3"; - ord_make_polynomial_in true thy substx (aa, bb); - true; (* => LESS *) - - val aa = (term_of o the o (parse thy)) "-1 * a * x"; - val bb = (term_of o the o (parse thy)) "x^^^3"; - ord_make_polynomial_in true thy substa (aa, bb); - false; (* => GREATER *) - - (*und nach dem Re-engineering der Termorders in den 'rulesets' - kannst Du die 'gr"osste' Variable frei w"ahlen: *) - val bdv= (term_of o the o (parse thy)) "bdv"; - val x = (term_of o the o (parse thy)) "x"; - val a = (term_of o the o (parse thy)) "a"; - val b = (term_of o the o (parse thy)) "b"; - val SOME (t',_) = - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2; -if term2str t' = "b + x + a" then () -else error "termorder.sml diff.behav ord_make_polynomial_in #11"; - - val NONE = - rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2; - term2str t'; - "a + x + b"; - - val SOME (t',_) = - rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2; -if term2str t' = "a + b + x" then () -else error "termorder.sml diff.behav ord_make_polynomial_in #13"; - - - - val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2"; - val ppp = (term_of o the o (parse thy)) ppp'; - val SOME (t',_) = - rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp; -(*MG 2003... - term2str t'; - "(-6) + (-5 * x + (-15 * x ^^^ 2))";*) -if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then () -else error "termorder.sml diff.behav ord_make_polynomial_in #14"; - - val SOME (t',_) = - rewrite_set_inst "Isac"false [("bdv","x")] "make_polynomial_in" ppp'; -(*MG 2003... - "(-6) + (-5 * x + (-15) * x ^^^ 2)";*) -if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then () -else error "termorder.sml diff.behav ord_make_polynomial_in #15"; - - val ttt' = "(3*x + 5)/18"; - val ttt = (term_of o the o (parse thy)) ttt'; - val SOME (uuu,_) = - rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt; -if term2str uuu = "(5 + 3 * x) / 18" then () -else error "termorder.sml diff.behav ord_make_polynomial_in #16"; - - val SOME (uuu,_) = - rewrite_set_ thy false make_polynomial ttt; -if term2str uuu = "(5 + 3 * x) / 18" then () -else error "termorder.sml diff.behav ord_make_polynomial_in #16"; - - - - -(*-----------28.2.03: war nicht upgedatet (und ausgeklammert in ROOT.ML - - (*Aufgabe zum Einstieg in die Arbeit...*) - val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0"; - (*ein 'ruleset' aus Poly.ML wird angewandt...*) - val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t; - term2str t; - "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0"; - val SOME (t,_) = - rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t; - term2str t; - "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0"; -(* bei Verwendung von "size_of-term" nach MG :*) -(*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *) - - (*wir holen 'a' wieder aus der Klammerung heraus...*) - val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t; - term2str t; - "x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0"; -(* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *) - - val SOME (t,_) = - rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t; - term2str t; - "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0"; - (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben - "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*) - - (*das rewriting l"asst sich beobachten mit - trace_rewrite:=true; - *) - - - -"------15.11.02 --------------------------"; - val t = (term_of o the o (parse thy)) "1 + a * x + b * x"; - val bdv = (term_of o the o (parse thy)) "bdv"; - val a = (term_of o the o (parse thy)) "a"; - - trace_rewrite:=true; - (* Anwenden einer Regelmenge aus Termorder.ML: *) - val SOME (t,_) = - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; - term2str t; - val SOME (t,_) = - rewrite_set_ thy false discard_parentheses t; - term2str t; -"1 + b * x + x * a"; - - val t = (term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2"; - val SOME (t,_) = - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; - term2str t; - val SOME (t,_) = - rewrite_set_ thy false discard_parentheses t; - term2str t; -"1 + (x + b * x) * a + a ^^^ 2"; - - val t = (term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2"; - val SOME (t,_) = - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; - term2str t; - val SOME (t,_) = - rewrite_set_ thy false discard_parentheses t; - term2str t; -"1 + b * a + (7 + x) * a ^^^ 2"; - -(* MG2003 - Atools.thy grundlegende Algebra - Poly.thy Polynome - Rational.thy Br"uche - Root.thy Wurzeln - RootRat.thy Wurzen + Br"uche - Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03) - - cd"knowledge"; - remove_thy"Termorder"; - use_thy"Isac"; - - get_thm Termorder.thy "bdv_n_collect"; - get_thm (theory "Isac") "bdv_n_collect"; - -*) - val t = (term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2"; - val SOME (t,_) = - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; - term2str t; - val SOME (t,_) = - rewrite_set_ thy false discard_parentheses t; - term2str t; -"(7 + x) * a ^^^ 2"; - - val t = (term_of o the o (parse Termorder.thy)) "Pi"; - - val t = (term_of o the o (parseold thy)) "7"; - -----------------------------------------------------------------------*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/test.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/Knowledge/test.sml Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,4 @@ +(* Title: test/../test.sml + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/trig.sml --- a/test/Tools/isac/Knowledge/trig.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Knowledge/trig.sml Wed Apr 06 18:01:02 2011 +0200 @@ -1,2 +1,7 @@ (* testexamples for Trig, trigonometry - *) \ No newline at end of file + *) +"--------------------------------------------------------"; +"table of contents --------------------------------------"; +"--------------------------------------------------------"; +"----------- TODO ---------------------------------------"; +"--------------------------------------------------------"; diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Knowledge/vect.sml --- a/test/Tools/isac/Knowledge/vect.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/Knowledge/vect.sml Wed Apr 06 18:01:02 2011 +0200 @@ -1,2 +1,7 @@ (* testexamples for Vect, vector spaces - *) \ No newline at end of file + *) +"--------------------------------------------------------"; +"table of contents --------------------------------------"; +"--------------------------------------------------------"; +"----------- TODO ---------------------------------------"; +"--------------------------------------------------------"; diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/ProgLang/rewrite.sml --- a/test/Tools/isac/ProgLang/rewrite.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/ProgLang/rewrite.sml Wed Apr 06 18:01:02 2011 +0200 @@ -23,6 +23,7 @@ "--------------------------------------------------------"; "--------------------------------------------------------"; +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. "----------- assemble rewrite ---------------------------"; "----------- assemble rewrite ---------------------------"; @@ -54,7 +55,6 @@ (*lookup in isabelle?trace?response...*) writeln(Syntax.string_of_term ctxt rew); writeln(Syntax.string_of_term ctxt RHS); - "===== rewriting: prep insertion into rew_sub"; val thy = @{theory Complex_Main}; val ctxt = @{context}; @@ -504,7 +504,6 @@ scan_ chk prepat; tracing "=== poly.sml: scan_ chk prepat end"; - "----- chk ---"; (*reestablish...*) val t = str2term "x ^^^ 2 * x"; val [(pres, pat)] = prepat; @@ -524,5 +523,4 @@ ([], true) => () | _ => error "rewrite.sml: diff. is_multUnordered, eval__true"; -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Test_Isac.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/Test_Isac.thy Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,157 @@ +(* Title: All tests on isac; observe outcommented + Author: Walther Neuper 101001 + (c) copyright due to lincense terms. + +$ cd /usr/local/isabisac/test/Tools/isac +$ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy & +*) + +theory Test_Isac imports Isac +uses + ( "library.sml") + ( "calcelems.sml") + ("ProgLang/termC.sml") + ("ProgLang/calculate.sml") + ("ProgLang/rewrite.sml") +(*("ProgLang/listg.sml") ("ProgLang/scrtools.sml") ("ProgLang/tools.sml") *) + + ("Interpret/mstools.sml") +(*("Interpret/ctree.sml")*) + ("Interpret/ptyps.sml") +(*("Interpret/generate.sml")*) + ("Interpret/calchead.sml") +(*("Interpret/appl.sml")*) + ("Interpret/rewtools.sml") +(*("Interpret/script.sml") + ("Interpret/solve.sml") + ("Interpret/inform.sml")*) + ("Interpret/mathengine.sml") + +(*("xmlsrc/mathml.sml") + ("xmlsrc/datatypes.sml") + ("xmlsrc/pbl-met-hierarchy.sml") + ("xmlsrc/thy-hierarchy.sml")*) + ("xmlsrc/interface-xml.sml") + + ("Frontend/messages.sml") + ("Frontend/states.sml") + ("Frontend/interface.sml") + ("print_exn_G.sml") + + ("Knowledge/delete.sml") + ("Knowledge/descript.sml") + ("Knowledge/atools.sml") + ("Knowledge/simplify.sml") + ("Knowledge/poly.sml") + ("Knowledge/rational.sml") + ("Knowledge/equation.sml") + ("Knowledge/root.sml") + ("Knowledge/lineq.sml") + ("Knowledge/rooteq.sml") + ("Knowledge/rateq.sml") + ("Knowledge/rootrateq.sml") +(*("Knowledge/polyeq.sml")*) + ("Knowledge/calculus.sml") + ("Knowledge/trig.sml") + ("Knowledge/logexp.sml") + ("Knowledge/diff.sml") + ("Knowledge/integrate.sml") + ("Knowledge/eqsystem.sml") + ("Knowledge/test.sml") + ("Knowledge/polyminus.sml") + ("Knowledge/vect.sml") + ("Knowledge/diffapp.sml") + ("Knowledge/biegelinie.sml") + ("Knowledge/algein.sml") + ("Knowledge/diophanteq.sml") + ("Knowledge/isac.sml") + + +begin + + ML {*print_depth 100*} + ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*} + use "library.sml" (*new 2011*) + use "calcelems.sml" (*complete*) + use "ProgLang/termC.sml" (*part.*) + use "ProgLang/calculate.sml" (*part.*) + use "ProgLang/rewrite.sml" (*part.*) +(*use "ProgLang/listg.sml" 2002*) +(*use "ProgLang/scrtools.sml" 2002*) +(*use "ProgLang/tools.sml" 2002*) + ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*} + ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*} + use "Interpret/mstools.sml" (*empty*) +(*use "Interpret/ctree.sml" TODO*) + use "Interpret/ptyps.sml" (* *) +(*use "Interpret/generate.sml" new 2011*) + use "Interpret/calchead.sml" (* *) +(*use "Interpret/appl.sml" new 2011*) + use "Interpret/rewtools.sml" (* *) +(*use "Interpret/script.sml" TODO*) +(*use "Interpret/solve.sml" TODO*) +(*use "Interpret/inform.sml" TODO*) + use "Interpret/mathengine.sml"(*part.*) + ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*} + ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*} +(*use "xmlsrc/mathml.sml" TODO*) +(*use "xmlsrc/datatypes.sml" TODO*) +(*use "xmlsrc/pbl-met-hierarchy.sml" TODO*) +(*use "xmlsrc/thy-hierarchy.sml" TODO after 2009-2*) + use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*) + ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*} + ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*} + use "Frontend/messages.sml" (*new 2011*) + use "Frontend/states.sml" (*new 2011*) + use "Frontend/interface.sml" (*part.*) + use "print_exn_G.sml" (*new 2011*) + ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*} + ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*} + use "Knowledge/delete.sml" (*new 2011*) + use "Knowledge/descript.sml" (*new 2011*) +(*use "Knowledge/atools.sml" 2002, added termorder.sml 2011*) + use "Knowledge/simplify.sml" (*part.*) +(*use "Knowledge/poly.sml" 2002*) +(*use "Knowledge/rational.sml" part.; diff.emacs--jedit*) +(*use "Knowledge/equation.sml" 2002*) +(*use "Knowledge/root.sml" 2002*) + use "Knowledge/lineq.sml" (*new 2011*) +(*use "Knowledge/rooteq.sml" 2002*) +(*use "Knowledge/rateq.sml" 2002*) +(*use "Knowledge/rootrat.sml" 2002*) +(*use "Knowledge/rootrateq.sml" 2002*) +(*use "Knowledge/polyeq.sml" 2002*) + use "Knowledge/calculus.sml" (*new 2011*) +(*use "Knowledge/trig.sml" 2002*) +(*use "Knowledge/logexp.sml" 2002*) + use "Knowledge/diff.sml" (*part.*) +(*use "Knowledge/integrate.sml" part. was complete 2009-2 + diff.emacs--jedit*) +(*use "Knowledge/eqsystem.sml" 2002*) + use "Knowledge/test.sml" (*new 2011*) + use "Knowledge/polyminus.sml" (*part.*) +(*use "Knowledge/vect.sml" 2002*) +(*use "Knowledge/diffapp.sml" 2002*) +(*use "Knowledge/biegelinie.sml" 2002*) +(*use "Knowledge/algein.sml" 2002*) + use "Knowledge/diophanteq.sml" (*complete*) + use "Knowledge/isac.sml" (*part.*) + ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*} + ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} + ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*} + ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} + +end + +(*=== inhibit exn ?============================================================= +===== inhibit exn ?===========================================================*) + +(*========== inhibit exn 110323 ================================================ + +"########### testcode inserted vvv ###########################################"; +"########### testcode inserted ^^^ ###########################################"; + +============ inhibit exn 110323 ==============================================*) + +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/Test_Some.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/Test_Some.thy Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,50 @@ +(* Title: Run_Tests as long Isac is not available: REPLACE 'IMPORTS' + Author: Walther Neuper 101001 + (c) copyright due to lincense terms. + +$ cd /usr/local/isabisac/test/Tools/isac +$ /usr/local/isabisac/bin/isabelle emacs Test_Some.thy & +*) + +theory Test_Some imports Isac begin +(*..................................########..................................*) + +ML {* +parse; +parseNEW; +update_loc'; +*} + + +ML{* writeln "**** run the test ***************************************" *} + +ML {* +fun term2st t = Print_Mode.setmp [] (Syntax.string_of_term +(ProofContext.init_global (Thy_Info.get_theory "Rational"))) t; +(*..............................................########......................*) +*} + +ML {*pos'2str; + + +*} + +use"../../../test/Tools/isac/Interpret/mstools.sml" + +end + + +(*=== inhibit exn ?============================================================= +===== inhibit exn ?===========================================================*) + + +(*========== inhibit exn 110317 ================================================ + +"########### testcode inserted vvv ###########################################"; +"########### testcode inserted ^^^ ###########################################"; + +============ inhibit exn 110317 ==============================================*) + + +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/library.sml --- a/test/Tools/isac/library.sml Mon Apr 04 11:05:07 2011 +0200 +++ b/test/Tools/isac/library.sml Wed Apr 06 18:01:02 2011 +0200 @@ -1,4 +1,9 @@ -{* +Toplevel.debug := true; + +fun term2st t = Print_Mode.setmp [] (Syntax.string_of_term +(ProofContext.init_global (Thy_Info.get_theory "Rational"))) t; +(*..............................................########......................*) + "--- Pure/General/ord_list.ML"; union; union (op =) [1,2,3] [3,4,5]; @@ -9,4 +14,4 @@ merge; merge (op =) ([1,2,3], [3,4,5]); (*val it = [4, 5, 1, 2, 3] : int list*) -*} + diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/print_exn_G.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/print_exn_G.sml Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,4 @@ +(* Title: test/../print_exn_G.sml + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*) diff -r c1859b72ae8d -r 2476f5f0f9ee test/Tools/isac/xmlsrc/interface-xml.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/xmlsrc/interface-xml.sml Wed Apr 06 18:01:02 2011 +0200 @@ -0,0 +1,4 @@ +(* Title: test/../interface-xml.sml + Author: Walther Neuper 110320 + (c) copyright due to lincense terms. +*)