1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-isac/mlehnfeld/master/ordered-KEStore_Elems.get_cas	Tue Nov 19 21:37:18 2013 +0000
     1.3 @@ -0,0 +1,6 @@
     1.4 +(Diff.Diff, ("Isac", ["derivative_of","function"], ["no_met"]))--1 
     1.5 +(Diff.Differentiate, ("Isac", ["named","derivative_of","function"], ["no_met"]))--4 
     1.6 +(Equation.solve, ("Isac", ["univariate","equation"], ["no_met"]))--3 
     1.7 +(Equation.solveTest, ("Test", ["univariate","equation","test"], ["no_met"]))--2 
     1.8 +(Simplify.Simplify, ("Isac", ["simplification"], ["no_met"]))--5 
     1.9 +(Simplify.Vereinfache, ("Isac", ["vereinfachen"], ["no_met"]))--6 
    1.10 \ No newline at end of file

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-isac/mlehnfeld/master/ordered-castab.Unsynchronized	Tue Nov 19 21:37:18 2013 +0000
     2.3 @@ -0,0 +1,6 @@
     2.4 +(Diff.Diff, ("Isac", ["derivative_of","function"], ["no_met"]))--2 
     2.5 +(Diff.Differentiate, ("Isac", ["named","derivative_of","function"], ["no_met"]))--1 
     2.6 +(Equation.solve, ("Isac", ["univariate","equation"], ["no_met"]))--3 
     2.7 +(Equation.solveTest, ("Test", ["univariate","equation","test"], ["no_met"]))--4 
     2.8 +(Simplify.Simplify, ("Isac", ["simplification"], ["no_met"]))--6 
     2.9 +(Simplify.Vereinfache, ("Isac", ["vereinfachen"], ["no_met"]))--5 
    2.10 \ No newline at end of file

     3.1 --- a/src/Tools/isac/KEStore.thy	Tue Nov 19 20:44:21 2013 +0000
     3.2 +++ b/src/Tools/isac/KEStore.thy	Tue Nov 19 21:37:18 2013 +0000
     3.3 @@ -120,6 +120,9 @@
     3.4  fun check_kestore_rls (rls', (thyID, rls)) =
     3.5    "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
     3.6  
     3.7 -fun check_kestore_calc ((id, (c, _)) : calc)  = "(" ^ id ^ ", (" ^ c ^ ", fn))"
     3.8 +fun check_kestore_calc ((id, (c, _)) : calc)  = "(" ^ id ^ ", (" ^ c ^ ", fn))";
     3.9 +
    3.10 +fun check_kestore_cas ((t, (s, _)):cas_elem) =
    3.11 +  "(" ^ (term_to_string''' @{theory} t) ^ ", " ^ (spec2str s) ^ ")";
    3.12  *}
    3.13  end

     4.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Tue Nov 19 20:44:21 2013 +0000
     4.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Tue Nov 19 21:37:18 2013 +0000
     4.3 @@ -9,28 +9,28 @@
     4.4  text {* This theory collects data of theorems and axioms defined and used in ISAC *}
     4.5  
     4.6  ML {*
     4.7 -  (*writeln ("======= length (KEStore_Elems = " ^
     4.8 -    string_of_int (length (KEStore_Elems.get_calcs @{theory})));
     4.9 -  writeln ("======= length (! calclist')   = " ^
    4.10 -    string_of_int (length (! calclist')));
    4.11 +  writeln ("======= length (KEStore_Elems = " ^
    4.12 +    string_of_int (length (KEStore_Elems.get_cas @{theory})));
    4.13 +  writeln ("======= length (! castab) = " ^
    4.14 +    string_of_int (length (! castab)));
    4.15  
    4.16    (* when creating session Isac see output in ~/.isabelle/../log/Isac *)
    4.17 -  writeln "======= begin KEStore_Elems.get_calcs @{theory} ======="; 
    4.18 -  KEStore_Elems.get_calcs @{theory} 
    4.19 -    |> map check_kestore_calc |> map writeln;
    4.20 -  writeln "======= KEStore_Elems.get_calcs @{theory} ordered ======="; 
    4.21 -  KEStore_Elems.get_calcs @{theory}
    4.22 -    |> map check_kestore_calc |> enumerate_strings |> sort string_ord |> map writeln;
    4.23 -  writeln "======= end KEStore_Elems.get_calcs @{theory} ======="; 
    4.24 +  writeln "======= begin KEStore_Elems.get_cas @{theory} =======";
    4.25 +  KEStore_Elems.get_cas @{theory}
    4.26 +    |> map check_kestore_cas |> map writeln;
    4.27 +  writeln "======= KEStore_Elems.get_cas @{theory} ordered =======";
    4.28 +  KEStore_Elems.get_cas @{theory}
    4.29 +    |> map check_kestore_cas |> enumerate_strings |> sort string_ord |> map writeln;
    4.30 +  writeln "======= end KEStore_Elems.get_cas @{theory} =======";
    4.31  
    4.32 -  (* use a diff-tool for comparing KEStore_Elems.get_rlss <--> ! xxx *)
    4.33 -  writeln "======= begin ! calclist' =======";
    4.34 -  ! calclist' |> rev (*!!!!!*)
    4.35 -    |> map check_kestore_calc |> map writeln;
    4.36 -  writeln "======= ! calclist' ordered =======";
    4.37 -  ! calclist' |> rev (*!!!!!*)
    4.38 -    |> map check_kestore_calc |> enumerate_strings |> sort string_ord |> map writeln;
    4.39 -  writeln "======= end ! calclist' =======";*)
    4.40 +  (* use a diff-tool for comparing KEStore_Elems.get_cas <--> ! xxx *)
    4.41 +  writeln "======= begin ! castab =======";
    4.42 +  ! castab |> rev (*!!!!!*)
    4.43 +    |> map check_kestore_cas |> map writeln;
    4.44 +  writeln "======= ! castab ordered =======";
    4.45 +  ! castab |> rev (*!!!!!*)
    4.46 +    |> map check_kestore_cas |> enumerate_strings |> sort string_ord |> map writeln;
    4.47 +  writeln "======= end ! calclist' =======";
    4.48  *}
    4.49  
    4.50  ML {*