1.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Sat Jan 20 15:07:58 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Sat Jan 20 15:18:41 2018 +0100
1.3 @@ -15,13 +15,11 @@
1.4 Make'_fun'_by'_new'_variable
1.5 :: "[real,real,bool list,
1.6 bool] => bool"
1.7 - ("((Script Make'_fun'_by'_new'_variable (_ _ _ =))//
1.8 - (_))" 9)
1.9 + ("((Script Make'_fun'_by'_new'_variable (_ _ _ =))// (_))" 9)
1.10 Make'_fun'_by'_explicit
1.11 :: "[real,real,bool list,
1.12 bool] => bool"
1.13 - ("((Script Make'_fun'_by'_explicit (_ _ _ =))//
1.14 - (_))" 9)
1.15 + ("((Script Make'_fun'_by'_explicit (_ _ _ =))// (_))" 9)
1.16
1.17 dummy :: real
1.18
2.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Sat Jan 20 15:07:58 2018 +0100
2.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Sat Jan 20 15:18:41 2018 +0100
2.3 @@ -12,12 +12,10 @@
2.4 (* subproblem and script-name *)
2.5 Ins'_sort :: "[int xlist,
2.6 int xlist] => int xlist"
2.7 - ("((Script Ins'_sort (_ =))//
2.8 - (_))" 9)
2.9 + ("((Script Ins'_sort (_ =))// (_))" 9)
2.10 Sortprog :: "[int xlist,
2.11 int xlist] => int xlist"
2.12 - ("((Script Sortprog (_ =))//
2.13 - (_))" 9)
2.14 + ("((Script Sortprog (_ =))// (_))" 9)
2.15
2.16 subsection {* functions *}
2.17 primrec ins :: "int \<Rightarrow> int xlist \<Rightarrow> int xlist"
3.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Sat Jan 20 15:07:58 2018 +0100
3.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Sat Jan 20 15:18:41 2018 +0100
3.3 @@ -13,8 +13,7 @@
3.4 Solve'_lineq'_equation
3.5 :: "[bool,real,
3.6 bool list] => bool list"
3.7 - ("((Script Solve'_lineq'_equation (_ _ =))//
3.8 - (_))" 9)
3.9 + ("((Script Solve'_lineq'_equation (_ _ =))// (_))" 9)
3.10
3.11 axiomatization where
3.12 (*-- normalize --*)
4.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sat Jan 20 15:07:58 2018 +0100
4.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Sat Jan 20 15:18:41 2018 +0100
4.3 @@ -23,8 +23,7 @@
4.4 Expand'_binoms
4.5 :: "['y,
4.6 'y] => 'y"
4.7 - ("((Script Expand'_binoms (_ =))//
4.8 - (_))" 9)
4.9 + ("((Script Expand'_binoms (_ =))// (_))" 9)
4.10
4.11 (*-------------------- rules------------------------------------------------*)
4.12 axiomatization where (*.not contained in Isabelle2002,
5.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Sat Jan 20 15:07:58 2018 +0100
5.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Sat Jan 20 15:18:41 2018 +0100
5.3 @@ -18,64 +18,52 @@
5.4 Complete'_square
5.5 :: "[bool,real,
5.6 bool list] => bool list"
5.7 - ("((Script Complete'_square (_ _ =))//
5.8 - (_))" 9)
5.9 + ("((Script Complete'_square (_ _ =))// (_))" 9)
5.10 (*----- poly ----- *)
5.11 Normalize'_poly
5.12 :: "[bool,real,
5.13 bool list] => bool list"
5.14 - ("((Script Normalize'_poly (_ _=))//
5.15 - (_))" 9)
5.16 + ("((Script Normalize'_poly (_ _=))// (_))" 9)
5.17 Solve'_d0'_polyeq'_equation
5.18 :: "[bool,real,
5.19 bool list] => bool list"
5.20 - ("((Script Solve'_d0'_polyeq'_equation (_ _ =))//
5.21 - (_))" 9)
5.22 + ("((Script Solve'_d0'_polyeq'_equation (_ _ =))// (_))" 9)
5.23 Solve'_d1'_polyeq'_equation
5.24 :: "[bool,real,
5.25 bool list] => bool list"
5.26 - ("((Script Solve'_d1'_polyeq'_equation (_ _ =))//
5.27 - (_))" 9)
5.28 + ("((Script Solve'_d1'_polyeq'_equation (_ _ =))// (_))" 9)
5.29 Solve'_d2'_polyeq'_equation
5.30 :: "[bool,real,
5.31 bool list] => bool list"
5.32 - ("((Script Solve'_d2'_polyeq'_equation (_ _ =))//
5.33 - (_))" 9)
5.34 + ("((Script Solve'_d2'_polyeq'_equation (_ _ =))// (_))" 9)
5.35 Solve'_d2'_polyeq'_sqonly'_equation
5.36 :: "[bool,real,
5.37 bool list] => bool list"
5.38 - ("((Script Solve'_d2'_polyeq'_sqonly'_equation (_ _ =))//
5.39 - (_))" 9)
5.40 + ("((Script Solve'_d2'_polyeq'_sqonly'_equation (_ _ =))// (_))" 9)
5.41 Solve'_d2'_polyeq'_bdvonly'_equation
5.42 :: "[bool,real,
5.43 bool list] => bool list"
5.44 - ("((Script Solve'_d2'_polyeq'_bdvonly'_equation (_ _ =))//
5.45 - (_))" 9)
5.46 + ("((Script Solve'_d2'_polyeq'_bdvonly'_equation (_ _ =))// (_))" 9)
5.47 Solve'_d2'_polyeq'_pq'_equation
5.48 :: "[bool,real,
5.49 bool list] => bool list"
5.50 - ("((Script Solve'_d2'_polyeq'_pq'_equation (_ _ =))//
5.51 - (_))" 9)
5.52 + ("((Script Solve'_d2'_polyeq'_pq'_equation (_ _ =))// (_))" 9)
5.53 Solve'_d2'_polyeq'_abc'_equation
5.54 :: "[bool,real,
5.55 bool list] => bool list"
5.56 - ("((Script Solve'_d2'_polyeq'_abc'_equation (_ _ =))//
5.57 - (_))" 9)
5.58 + ("((Script Solve'_d2'_polyeq'_abc'_equation (_ _ =))// (_))" 9)
5.59 Solve'_d3'_polyeq'_equation
5.60 :: "[bool,real,
5.61 bool list] => bool list"
5.62 - ("((Script Solve'_d3'_polyeq'_equation (_ _ =))//
5.63 - (_))" 9)
5.64 + ("((Script Solve'_d3'_polyeq'_equation (_ _ =))// (_))" 9)
5.65 Solve'_d4'_polyeq'_equation
5.66 :: "[bool,real,
5.67 bool list] => bool list"
5.68 - ("((Script Solve'_d4'_polyeq'_equation (_ _ =))//
5.69 - (_))" 9)
5.70 + ("((Script Solve'_d4'_polyeq'_equation (_ _ =))// (_))" 9)
5.71 Biquadrat'_poly
5.72 :: "[bool,real,
5.73 bool list] => bool list"
5.74 - ("((Script Biquadrat'_poly (_ _=))//
5.75 - (_))" 9)
5.76 + ("((Script Biquadrat'_poly (_ _=))// (_))" 9)
5.77
5.78 (*-------------------- rules -------------------------------------------------*)
5.79 (* type real enforced by op "^^^" *)
6.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Sat Jan 20 15:07:58 2018 +0100
6.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Sat Jan 20 15:18:41 2018 +0100
6.3 @@ -29,8 +29,7 @@
6.4 Solve'_rat'_equation
6.5 :: "[bool,real,
6.6 bool list] => bool list"
6.7 - ("((Script Solve'_rat'_equation (_ _ =))//
6.8 - (_))" 9)
6.9 + ("((Script Solve'_rat'_equation (_ _ =))// (_))" 9)
6.10
6.11 axiomatization where
6.12 (* FIXME also in Poly.thy def. --> FIXED*)
7.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Sat Jan 20 15:07:58 2018 +0100
7.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Sat Jan 20 15:18:41 2018 +0100
7.3 @@ -29,23 +29,19 @@
7.4 Norm'_sq'_root'_equation
7.5 :: "[bool,real,
7.6 bool list] => bool list"
7.7 - ("((Script Norm'_sq'_root'_equation (_ _ =))//
7.8 - (_))" 9)
7.9 + ("((Script Norm'_sq'_root'_equation (_ _ =))// (_))" 9)
7.10 Solve'_sq'_root'_equation
7.11 :: "[bool,real,
7.12 bool list] => bool list"
7.13 - ("((Script Solve'_sq'_root'_equation (_ _ =))//
7.14 - (_))" 9)
7.15 + ("((Script Solve'_sq'_root'_equation (_ _ =))// (_))" 9)
7.16 Solve'_left'_sq'_root'_equation
7.17 :: "[bool,real,
7.18 bool list] => bool list"
7.19 - ("((Script Solve'_left'_sq'_root'_equation (_ _ =))//
7.20 - (_))" 9)
7.21 + ("((Script Solve'_left'_sq'_root'_equation (_ _ =))// (_))" 9)
7.22 Solve'_right'_sq'_root'_equation
7.23 :: "[bool,real,
7.24 bool list] => bool list"
7.25 - ("((Script Solve'_right'_sq'_root'_equation (_ _ =))//
7.26 - (_))" 9)
7.27 + ("((Script Solve'_right'_sq'_root'_equation (_ _ =))// (_))" 9)
7.28
7.29 axiomatization where
7.30
8.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Sat Jan 20 15:07:58 2018 +0100
8.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Sat Jan 20 15:18:41 2018 +0100
8.3 @@ -24,8 +24,7 @@
8.4 Elim'_rootrat'_equation
8.5 :: "[bool,real,
8.6 bool list] => bool list"
8.7 - ("((Script Elim'_rootrat'_equation (_ _ =))//
8.8 - (_))" 9)
8.9 + ("((Script Elim'_rootrat'_equation (_ _ =))// (_))" 9)
8.10 (*-------------------- rules------------------------------------------------*)
8.11
8.12 axiomatization where
9.1 --- a/src/Tools/isac/Knowledge/Test.thy Sat Jan 20 15:07:58 2018 +0100
9.2 +++ b/src/Tools/isac/Knowledge/Test.thy Sat Jan 20 15:18:41 2018 +0100
9.3 @@ -12,20 +12,17 @@
9.4 Expand'_binomtest
9.5 :: "['y,
9.6 'y] => 'y"
9.7 - ("((Script Expand'_binomtest (_ =))//
9.8 - (_))" 9)
9.9 + ("((Script Expand'_binomtest (_ =))// (_))" 9)
9.10
9.11 Solve'_univar'_err
9.12 :: "[bool,real,bool,
9.13 bool list] => bool list"
9.14 - ("((Script Solve'_univar'_err (_ _ _ =))//
9.15 - (_))" 9)
9.16 + ("((Script Solve'_univar'_err (_ _ _ =))// (_))" 9)
9.17
9.18 Solve'_linear
9.19 :: "[bool,real,
9.20 bool list] => bool list"
9.21 - ("((Script Solve'_linear (_ _ =))//
9.22 - (_))" 9)
9.23 + ("((Script Solve'_linear (_ _ =))// (_))" 9)
9.24
9.25 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)
9.26
9.27 @@ -40,26 +37,22 @@
9.28 Solve'_root'_equation
9.29 :: "[bool,real,
9.30 bool list] => bool list"
9.31 - ("((Script Solve'_root'_equation (_ _ =))//
9.32 - (_))" 9)
9.33 + ("((Script Solve'_root'_equation (_ _ =))// (_))" 9)
9.34
9.35 Solve'_plain'_square
9.36 :: "[bool,real,
9.37 bool list] => bool list"
9.38 - ("((Script Solve'_plain'_square (_ _ =))//
9.39 - (_))" 9)
9.40 + ("((Script Solve'_plain'_square (_ _ =))// (_))" 9)
9.41
9.42 Norm'_univar'_equation
9.43 :: "[bool,real,
9.44 bool] => bool"
9.45 - ("((Script Norm'_univar'_equation (_ _ =))//
9.46 - (_))" 9)
9.47 + ("((Script Norm'_univar'_equation (_ _ =))// (_))" 9)
9.48
9.49 STest'_simplify
9.50 :: "['z,
9.51 'z] => 'z"
9.52 - ("((Script STest'_simplify (_ =))//
9.53 - (_))" 9)
9.54 + ("((Script STest'_simplify (_ =))// (_))" 9)
9.55
9.56 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)
9.57
10.1 --- a/src/Tools/isac/ProgLang/Script.thy Sat Jan 20 15:07:58 2018 +0100
10.2 +++ b/src/Tools/isac/ProgLang/Script.thy Sat Jan 20 15:18:41 2018 +0100
10.3 @@ -112,20 +112,16 @@
10.4 ----------*)
10.5
10.6 Testeq :: "[bool, bool] => bool"
10.7 - ("((Script Testeq (_ =))//
10.8 - (_))" 9)
10.9 + ("((Script Testeq (_ =))// (_))" 9)
10.10
10.11 Testeq2 :: "[bool, bool list] => bool list"
10.12 - ("((Script Testeq2 (_ =))//
10.13 - (_))" 9)
10.14 + ("((Script Testeq2 (_ =))// (_))" 9)
10.15
10.16 Testterm :: "[real, real] => real"
10.17 - ("((Script Testterm (_ =))//
10.18 - (_))" 9)
10.19 + ("((Script Testterm (_ =))// (_))" 9)
10.20
10.21 Testchk :: "[bool, real, real list] => real list"
10.22 - ("((Script Testchk (_ _ =))//
10.23 - (_))" 9)
10.24 + ("((Script Testchk (_ _ =))// (_))" 9)
10.25 (*... + RECORD IN 'subpbls' in Script.ML *)
10.26 (*SHIFT -> resp.thys ----^^^----------------------------*)
10.27