1.1 --- a/test/Pure/term_xml_Try.thy Mon Jul 19 15:34:54 2021 +0200
1.2 +++ b/test/Pure/term_xml_Try.thy Mon Jul 19 17:29:35 2021 +0200
1.3 @@ -2,10 +2,12 @@
1.4
1.5 ML\<open>
1.6 @{term "aaa + bbb"}
1.7 -(* = Const ("Groups.plus_class.plus", "'a \<Rightarrow> 'a \<Rightarrow> 'a") $ Free ("aaa", "'a") $ Free ("bbb", "'a")*)
1.8 +(* = (\<^const_name>\<open>plus\<close>, "'a \<Rightarrow> 'a \<Rightarrow> 'a") $ Free ("aaa", "'a") $ Free ("bbb", "'a")*)
1.9 \<close>
1.10 declare[[ML_print_depth = 999]]
1.11 -ML\<open>
1.12 +text\<open> broken by (\<^const_name>\<open>plus\<close>, _) -->
1.13 + Const (\ <^const_name>\<open>divide_class.divide\<close>, _)
1.14 + DEPRECATED
1.15 Term_XML.Encode.term @{term "aaa + bbb"}
1.16 (* = [
1.17 <5>
2.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Mon Jul 19 15:34:54 2021 +0200
2.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Mon Jul 19 17:29:35 2021 +0200
2.3 @@ -23,14 +23,14 @@
2.4 * ("Rational.get_denominator", eval_get_denominator ""))
2.5 *)
2.6 fun eval_get_denominator (thmid:string) _
2.7 - (t as Const ("Rational.get_denominator", _) $
2.8 - (Const (\<^const_name>\<open>divide\<close>, _) $num
2.9 + (t as Const (\<^const_name>\<open>Rational.get_denominator\<close>, _) $
2.10 + (Const (\<^const_name>\<open>divide\<close>, _) $ num
2.11 $denom)) thy =
2.12 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy denom) "",
2.13 HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
2.14 | eval_get_denominator _ _ _ _ = NONE;
2.15 \<close>
2.16 -(*----END----Example Function Decleration from Rationals.thy----*)
2.17 +(*----END----Example Function Declaration from Rationals.thy----*)
2.18
2.19 text\<open>Apply the MethodC to an expression.\<close>
2.20
3.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Jul 19 15:34:54 2021 +0200
3.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Jul 19 17:29:35 2021 +0200
3.3 @@ -80,9 +80,11 @@
3.4 ];
3.5
3.6 \<close> ML \<open>
3.7 - val t = TermC.str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
3.8 + val t = TermC.str2term "z / (z - 1) + z / (z - \<alpha>) + 1::real";
3.9 \<close> ML \<open>
3.10 val SOME (t', asm) = Rewrite.rewrite_set_ thy true inverse_Z t;
3.11 +(*rewrite__set_ called with 'Erls' for '|| z || < 1'*)
3.12 +\<close> ML \<open>
3.13 UnparseC.term t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
3.14 (*
3.15 * Attention rule1 is applied before the expression is
3.16 @@ -216,7 +218,7 @@
3.17 * ("Rational.get_denominator", eval_get_denominator ""))
3.18 *)
3.19 fun eval_get_denominator (thmid:string) _
3.20 - (t as Const ("Rational.get_denominator", _) $
3.21 + (t as Const (\<^const_name>\<open>get_denominator\<close>, _) $
3.22 (Const (\<^const_name>\<open>divide\<close>, _) $num
3.23 $denom)) thy =
3.24 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy denom) "",
3.25 @@ -236,7 +238,7 @@
3.26 * ("Rational.get_numerator", eval_get_numerator ""))
3.27 *)
3.28 fun eval_get_numerator (thmid:string) _
3.29 - (t as Const ("Rational.get_numerator", _) $
3.30 + (t as Const (\<^const_name>\<open>Rational.get_numerator\<close>, _) $
3.31 (Const (\<^const_name>\<open>divide\<close>, _) $num
3.32 $denom )) thy =
3.33 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy num) "",
4.1 --- a/test/Tools/isac/BaseDefinitions/substitution.sml Mon Jul 19 15:34:54 2021 +0200
4.2 +++ b/test/Tools/isac/BaseDefinitions/substitution.sml Mon Jul 19 17:29:35 2021 +0200
4.3 @@ -74,9 +74,9 @@
4.4 [(Free ("bdv_1", _), Free ("x", _)),
4.5 (Free ("bdv_2", _), Free ("y", _)),
4.6 (Free ("xxx", _),
4.7 - Const ("Groups.plus_class.plus", _) $ Free ("aaa", _) $
4.8 - (Const ("Num.numeral_class.numeral", _) $
4.9 - (Const ("Num.num.Bit1", _) $ _ )))] => ()
4.10 + Const (\<^const_name>\<open>plus_class.plus\<close>, _) $ Free ("aaa", _) $
4.11 + (Const (\<^const_name>\<open>numeral\<close>, _) $
4.12 + (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ _ )))] => ()
4.13 | _ => error "fun T_from_string_eqs";
4.14
4.15 "-------- fun input_to_terms -------------------------------------------------";
4.16 @@ -87,7 +87,7 @@
4.17
4.18 case Subst.input_to_terms input of
4.19 [Const (\<^const_name>\<open>Pair\<close>, _) $
4.20 - (Const (\<^const_name>\<open>Cons\<close>, _) $ (Const ("String.char.Char", _) $
4.21 + (Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>Char\<close>, _) $
4.22 Const (\<^const_name>\<open>False\<close>, _) $ _ $ _ $ _ $ _ $ _ $ _ $ _) $ _) $
4.23 Free ("x", _),
4.24 _,
5.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Mon Jul 19 15:34:54 2021 +0200
5.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Mon Jul 19 17:29:35 2021 +0200
5.3 @@ -40,9 +40,9 @@
5.4 "***Isabelle2011 ~= Isabelle2012 = Isabelle2013";
5.5 "***Isabelle2011**********************************************************************************";
5.6 @{term "0::nat"};
5.7 -(*Const ("Groups.zero_class.zero", "Nat.nat")*)
5.8 +(*Const (\<^const_name>\<open>zero_class.zero\<close>, "Nat.nat")*)
5.9 @{term "1::nat"};
5.10 -(*Const ("Groups.one_class.one", "Nat.nat")*)
5.11 +(*Const (\<^const_name>\<open>one_class.one\<close>, "Nat.nat")*)
5.12 @{term "5::nat"};
5.13 (*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> Nat.nat") $
5.14 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
5.15 @@ -50,9 +50,9 @@
5.16 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)
5.17 (*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)
5.18 @{term "0::int"};
5.19 -(*Const ("Groups.zero_class.zero", "Int.int")*)
5.20 +(*Const (\<^const_name>\<open>zero_class.zero\<close>, "Int.int")*)
5.21 @{term "1::int"};
5.22 -(*Const ("Groups.one_class.one", "Int.int")*)
5.23 +(*Const (\<^const_name>\<open>one_class.one\<close>, "Int.int")*)
5.24 @{term "5::int"};
5.25 (*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> Int.int") $
5.26 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
5.27 @@ -64,14 +64,14 @@
5.28 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
5.29 (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)
5.30 @{term "- 5::int"};
5.31 -(*Const ("Groups.uminus_class.uminus", "Int.int \<Rightarrow> Int.int") $
5.32 +(*Const (\<^const_name>\<open>uminus\<close>, "Int.int \<Rightarrow> Int.int") $
5.33 (Const ("Int.number_class.number_of", "Int.int \<Rightarrow> Int.int") $
5.34 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
5.35 (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
5.36 (Const ("Int.Bit1...", "Int.int \<Rightarrow> Int.int") $ Const (...)))))*)
5.37 (*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)
5.38 @{term "0::real"};
5.39 -(*Const ("Groups.zero_class.zero", "Real.real")*)
5.40 +(*Const (\<^const_name>\<open>zero_class.zero\<close>, "Real.real")*)
5.41 @{term "1::real"};
5.42 (**)
5.43 @{term "5::real"};
5.44 @@ -85,101 +85,101 @@
5.45 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
5.46 (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)
5.47 @{term "- 5::real"};
5.48 -(*Const ("Groups.uminus_class.uminus", "Real.real \<Rightarrow> "Real.real") $
5.49 +(*Const (\<^const_name>\<open>uminus\<close>, "Real.real \<Rightarrow> "Real.real") $
5.50 (Const ("Int.number_class.number_of", "Int.int \<Rightarrow> "Real.real") $
5.51 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
5.52 (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
5.53 (Const ("Int.Bit1...", "Int.int \<Rightarrow> Int.int") $ Const (...)))))*)
5.54 "***Isabelle2012**********************************************************************************";
5.55 @{term "0::nat"};
5.56 -(*Const ("Groups.zero_class.zero", "nat")*)
5.57 +(*Const (\<^const_name>\<open>zero_class.zero\<close>, "nat")*)
5.58 @{term "1::nat"};
5.59 -(*Const ("Groups.one_class.one", "nat")*)
5.60 +(*Const (\<^const_name>\<open>one_class.one\<close>, "nat")*)
5.61 @{term "5::nat"};
5.62 -(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> nat") $
5.63 - (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
5.64 - (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
5.65 +(*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> nat") $
5.66 + (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $
5.67 + (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)
5.68 (*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)
5.69 @{term "0::int"};
5.70 -(*Const ("Groups.zero_class.zero", "int")*)
5.71 +(*Const (\<^const_name>\<open>zero_class.zero\<close>, "int")*)
5.72 @{term "1::int"};
5.73 -(*Const ("Groups.one_class.one", "int")*)
5.74 +(*Const (\<^const_name>\<open>one_class.one\<close>, "int")*)
5.75 @{term "5::int"};
5.76 -(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> int") $
5.77 - (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
5.78 - (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
5.79 +(*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> int") $
5.80 + (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $
5.81 + (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)
5.82 @{term "-5::int"};
5.83 (*Const ("Num.neg_numeral_class.neg_numeral", "num \<Rightarrow> int") $
5.84 - (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
5.85 - (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
5.86 + (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $
5.87 + (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)
5.88 @{term "- 5::int"};
5.89 -(*Const ("Groups.uminus_class.uminus", "int \<Rightarrow> int") $
5.90 - (Const ("Num.numeral_class.numeral", "num \<Rightarrow> int") $
5.91 - (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
5.92 - (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("...", "num"))))*)
5.93 +(*Const (\<^const_name>\<open>uminus\<close>, "int \<Rightarrow> int") $
5.94 + (Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> int") $
5.95 + (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $
5.96 + (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const ("...", "num"))))*)
5.97 (*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)
5.98 @{term "0::real"};
5.99 -(*Const ("Groups.zero_class.zero", "real")*)
5.100 +(*Const (\<^const_name>\<open>zero_class.zero\<close>, "real")*)
5.101 @{term "1::real"};
5.102 -(*Const ("Groups.one_class.one", "real")*)
5.103 +(*Const (\<^const_name>\<open>one_class.one\<close>, "real")*)
5.104 @{term "5::real"};
5.105 -(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $
5.106 - (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
5.107 - (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
5.108 +(*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> real") $
5.109 + (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $
5.110 + (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)
5.111 @{term "-5::real"};
5.112 (*Const ("Num.neg_numeral_class.neg_numeral", "num \<Rightarrow> real") $
5.113 - (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
5.114 - (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
5.115 + (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $
5.116 + (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)
5.117 @{term "- 5::real"};
5.118 -(*Const ("Groups.uminus_class.uminus", "real \<Rightarrow> real") $
5.119 - (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $
5.120 - (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
5.121 - (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("...", "num"))))*)
5.122 +(*Const (\<^const_name>\<open>uminus\<close>, "real \<Rightarrow> real") $
5.123 + (Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> real") $
5.124 + (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $
5.125 + (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const ("...", "num"))))*)
5.126 "***Isabelle2013**********************************************************************************";
5.127 @{term "0::nat"};
5.128 -(*Const ("Groups.zero_class.zero", "nat")*)
5.129 +(*Const (\<^const_name>\<open>zero_class.zero\<close>, "nat")*)
5.130 @{term "1::nat"};
5.131 -(*Const ("Groups.one_class.one", "nat")*)
5.132 +(*Const (\<^const_name>\<open>one_class.one\<close>, "nat")*)
5.133 @{term "5::nat"};
5.134 -(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> nat") $
5.135 - (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
5.136 - (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
5.137 +(*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> nat") $
5.138 + (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $
5.139 + (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)
5.140 (*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)
5.141 @{term "0::int"};
5.142 -(*Const ("Groups.zero_class.zero", "int")*)
5.143 +(*Const (\<^const_name>\<open>zero_class.zero\<close>, "int")*)
5.144 @{term "1::int"};
5.145 -(*Const ("Groups.one_class.one", "int")*)
5.146 +(*Const (\<^const_name>\<open>one_class.one\<close>, "int")*)
5.147 @{term "5::int"};
5.148 -(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> int") $
5.149 - (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
5.150 - (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
5.151 +(*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> int") $
5.152 + (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $
5.153 + (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)
5.154 @{term "-5::int"};
5.155 (*Const ("Num.neg_numeral_class.neg_numeral", "num \<Rightarrow> int") $
5.156 - (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
5.157 - (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
5.158 + (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $
5.159 + (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)
5.160 @{term "- 5::int"};
5.161 -(*Const ("Groups.uminus_class.uminus", "int \<Rightarrow> int") $
5.162 - (Const ("Num.numeral_class.numeral", "num \<Rightarrow> int") $
5.163 - (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
5.164 - (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("...", "num"))))*)
5.165 +(*Const (\<^const_name>\<open>uminus\<close>, "int \<Rightarrow> int") $
5.166 + (Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> int") $
5.167 + (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $
5.168 + (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const ("...", "num"))))*)
5.169 (*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)
5.170 @{term "0::real"};
5.171 -(*Const ("Groups.zero_class.zero", "real")*)
5.172 +(*Const (\<^const_name>\<open>zero_class.zero\<close>, "real")*)
5.173 @{term "1::real"};
5.174 -(*Const ("Groups.one_class.one", "real")*)
5.175 +(*Const (\<^const_name>\<open>one_class.one\<close>, "real")*)
5.176 @{term "5::real"};
5.177 -(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $
5.178 - (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
5.179 - (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
5.180 +(*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> real") $
5.181 + (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $
5.182 + (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)
5.183 @{term "-5::real"};
5.184 (*Const ("Num.neg_numeral_class.neg_numeral", "num \<Rightarrow> real") $
5.185 - (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
5.186 - (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
5.187 + (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $
5.188 + (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)
5.189 @{term "- 5::real"};
5.190 -(*Const ("Groups.uminus_class.uminus", "real \<Rightarrow> real") $
5.191 - (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $
5.192 - (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
5.193 - (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("...", "num"))))*)
5.194 +(*Const (\<^const_name>\<open>uminus\<close>, "real \<Rightarrow> real") $
5.195 + (Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> real") $
5.196 + (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $
5.197 + (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const ("...", "num"))))*)
5.198
5.199 "----------- inst_bdv -----------------------------------";
5.200 "----------- inst_bdv -----------------------------------";
5.201 @@ -413,7 +413,7 @@
5.202
5.203 val SOME t = TermC.parseNEW ctxt "3 = 3 * AA / 4";
5.204
5.205 -case TermC.vars_of t of [Const ("Partial_Fractions.AA", _), Const (\<^const_name>\<open>HOL.eq\<close>, _)] => ()
5.206 +case TermC.vars_of t of [Const (\<^const_name>\<open>AA\<close>, _), Const (\<^const_name>\<open>HOL.eq\<close>, _)] => ()
5.207 | _ => error "TermC.vars_of (3 = 3 * AA / 4) ..changed (! use only for polynomials, not equations!)";
5.208
5.209
5.210 @@ -689,18 +689,18 @@
5.211 "----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------";
5.212 "----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------";
5.213 case ThmC_Def.num_to_Free @{term "123::real"} of
5.214 - Const ("Num.numeral_class.numeral", _) $
5.215 - (Const ("Num.num.Bit1", _) $
5.216 - (Const ("Num.num.Bit1", _) $
5.217 - (Const ("Num.num.Bit0", _) $ (Const ("Num.num.Bit1", _) $ (Const ("Num.num.Bit1", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _))))))) => ()
5.218 + Const (\<^const_name>\<open>numeral\<close>, _) $
5.219 + (Const (\<^const_name>\<open>num.Bit1\<close>, _) $
5.220 + (Const (\<^const_name>\<open>num.Bit1\<close>, _) $
5.221 + (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))))))) => ()
5.222 | _ => error "ThmC_Def.num_to_Free '123' changed";
5.223
5.224 case ThmC_Def.num_to_Free @{term "1::real"} of
5.225 - Const ("Groups.one_class.one", _) => ()
5.226 + Const (\<^const_name>\<open>one_class.one\<close>, _) => ()
5.227 | _ => error "ThmC_Def.num_to_Free '1' changed";
5.228
5.229 case ThmC_Def.num_to_Free @{term "0::real"} of
5.230 - Const ("Groups.zero_class.zero", _) => ()
5.231 + Const (\<^const_name>\<open>zero_class.zero\<close>, _) => ()
5.232 | _ => error "ThmC_Def.num_to_Free '0' changed";
5.233
5.234 "----------- fun mk_frac, proper term with uminus ----------------------------------------------";
5.235 @@ -709,15 +709,15 @@
5.236 TermC.mk_frac: typ -> int * (int * int) -> term;
5.237 TermC.mk_frac HOLogic.realT (~1, (6, 8));
5.238 "~~~~~ fun mk_frac , args:"; val (T, (sg, (i1, i2))) = (HOLogic.realT, (~1, (6, 8)));
5.239 -val xxx = (*return value*) Const ("Rings.divide_class.divide", T --> T) $
5.240 +val xxx = (*return value*) Const (\<^const_name>\<open>divide\<close>, T --> T) $
5.241 mk_negative T (HOLogic.mk_number T i1) $ HOLogic.mk_number T i2;
5.242
5.243 val (T_div, T_uminus) =
5.244 case xxx of
5.245 - Const ("Rings.divide_class.divide", T_div) $ (* divide *)
5.246 - (Const ("Groups.uminus_class.uminus", T_uminus) $ (* uminus *)
5.247 - (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ _ ))) $
5.248 - (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ _ ))
5.249 + Const (\<^const_name>\<open>divide\<close>, T_div) $ (* divide *)
5.250 + (Const (\<^const_name>\<open>uminus\<close>, T_uminus) $ (* uminus *)
5.251 + (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ _ ))) $
5.252 + (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ _ ))
5.253 => (T_div, T_uminus)
5.254 | _ => error "mk_frac 6 / - 8 \<longrightarrow> - 3 / 4 CHANGED";
5.255
5.256 @@ -730,8 +730,8 @@
5.257
5.258 (* IMproper term for "6 / - 8 = - 3 / (4::real)"
5.259
5.260 - (Const ("Groups.uminus_class.uminus", _) $ (* uminus *)
5.261 - (Const ("Rings.divide_class.divide", _) $ (* divide *)
5.262 - (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ _ ))) $
5.263 - (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ _ ) ))))
5.264 + (Const (\<^const_name>\<open>uminus\<close>, _) $ (* uminus *)
5.265 + (Const (\<^const_name>\<open>divide\<close>, _) $ (* divide *)
5.266 + (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ _ ))) $
5.267 + (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ _ ) ))))
5.268 *)
6.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Mon Jul 19 15:34:54 2021 +0200
6.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Mon Jul 19 17:29:35 2021 +0200
6.3 @@ -48,8 +48,8 @@
6.4 (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + - 1 * ?b"),
6.5 Thm ("Delete.real_mult_minus1", "- 1 * ?z = - ?z")] : rule list*)
6.6 |> map (fn Thm (thmID, thm) => (thmID, Thm.prop_of thm))
6.7 - (* = [("Poly.real_diff_minus", Const ("HOL.Trueprop", "bool \<Rightarrow> prop") $ ...,
6.8 - ("Delete.real_mult_minus1", Const ("HOL.Trueprop", ...)] : (string * term) list*)
6.9 + (* = [("Poly.real_diff_minus", Const (\<^const_name>\<open>Trueprop\<close>, "bool \<Rightarrow> prop") $ ...,
6.10 + ("Delete.real_mult_minus1", Const (\<^const_name>\<open>Trueprop\<close>, ...)] : (string * term) list*)
6.11 |> distinct (fn ((thmID1, thm1), (thmID2, thm2)) => thmID1 = thmID2);
6.12
6.13
7.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Mon Jul 19 15:34:54 2021 +0200
7.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Mon Jul 19 17:29:35 2021 +0200
7.3 @@ -638,7 +638,7 @@
7.4 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
7.5 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
7.6 val t = TermC.str2term "Diff (x \<up> 2 + x + 1, x)";
7.7 -case t of Const ("Diff.Diff", _) $ _ => ()
7.8 +case t of Const (\<^const_name>\<open>Diff\<close>, _) $ _ => ()
7.9 | _ => raise
7.10 error "diff.sml behav.changed for CAS Diff (..., x)";
7.11 TermC.atomty t;
8.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Jul 19 15:34:54 2021 +0200
8.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Jul 19 17:29:35 2021 +0200
8.3 @@ -139,11 +139,11 @@
8.4 = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
8.5
8.6 (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
8.7 -"~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a))
8.8 +"~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const (\<^const_name>\<open>Chain\<close>(*1*), _) $ e1 $ e2 $ a))
8.9 = (xxx, (ist |> path_down [L, R]), e);
8.10
8.11 (*case*) scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
8.12 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))
8.13 +"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
8.14 = (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
8.15
8.16 (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
8.17 @@ -307,7 +307,7 @@
8.18 (*if*) 1 < length path (*then*);
8.19
8.20 scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
8.21 -"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const ("Tactical.Try"(*2*), _) $ _))
8.22 +"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ _))
8.23 = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
8.24
8.25 go_scan_up1 pcct ist;
8.26 @@ -317,16 +317,16 @@
8.27
8.28 scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
8.29 "~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, _, _))), ist,
8.30 - (Const ("Tactical.Chain"(*3*), _) $ _ ))
8.31 + (Const (\<^const_name>\<open>Chain\<close>(*3*), _) $ _ ))
8.32 = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
8.33 val e2 = check_Seq_up ist prog
8.34 ;
8.35 (*case*) scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 (*of*);
8.36 -"~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const ("Tactical.Chain"(*2*), _) $ e1 $ e2))
8.37 +"~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ e1 $ e2))
8.38 = (cct, (ist |> path_up_down [R] |> set_or ORundef), e2);
8.39
8.40 (*case*) scan_dn1 cct (ist |> path_down [L, R]) e1 (*of*);
8.41 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))
8.42 +"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
8.43 = (cct, (ist |> path_down [L, R]), e1);
8.44
8.45 (*case*) scan_dn1 cct (ist |> path_down [R]) e (*of*);
9.1 --- a/test/Tools/isac/Knowledge/integrate.sml Mon Jul 19 15:34:54 2021 +0200
9.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Mon Jul 19 17:29:35 2021 +0200
9.3 @@ -54,12 +54,12 @@
9.4 val t = str2t "Integral x D x";
9.5 val t = str2t "Integral x \<up> 2 D x";
9.6 case t of
9.7 - Const ("Integrate.Integral", _) $
9.8 + Const (\<^const_name>\<open>Integral\<close>, _) $
9.9 (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ Free _) $ Free ("x", _) => ()
9.10 | _ => error "integrate.sml: parsing: Integral x \<up> 2 D x";
9.11
9.12 val t = str2t "ff x is_f_x";
9.13 -case t of Const ("Integrate.is_f_x", _) $ _ => ()
9.14 +case t of Const (\<^const_name>\<open>is_f_x\<close>, _) $ _ => ()
9.15 | _ => error "integrate.sml: parsing: ff x is_f_x";
9.16
9.17
9.18 @@ -340,7 +340,7 @@
9.19 val t1 = (Thm.term_of o hd) chkmodel;
9.20 val t2 = (Thm.term_of o hd o tl) chkmodel;
9.21 val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
9.22 -case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()
9.23 +case t3 of Const (\<^const_name>\<open>antiDerivative\<close>, _) $ _ => ()
9.24 | _ => error "integrate.sml: Integrate.antiDerivative ???";
9.25
9.26 val model = {Given =["functionTerm f_f", "integrateBy v_v"],
9.27 @@ -352,18 +352,18 @@
9.28 val t1 = (Thm.term_of o hd) chkmodel;
9.29 val t2 = (Thm.term_of o hd o tl) chkmodel;
9.30 val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
9.31 -case t3 of Const ("Integrate.antiDerivativeName", _) $ _ => ()
9.32 +case t3 of Const (\<^const_name>\<open>antiDerivativeName\<close>, _) $ _ => ()
9.33 | _ => error "integrate.sml: Integrate.antiDerivativeName";
9.34
9.35 "----- compare 'Find's from problem, script, formalization -------";
9.36 val {ppc,...} = Problem.from_store ["named", "integrate", "function"];
9.37 -val ("#Find", (Const ("Integrate.antiDerivativeName", _),
9.38 +val ("#Find", (Const (\<^const_name>\<open>antiDerivativeName\<close>, _),
9.39 F1_ as Free ("F_F", F1_type))) = last_elem ppc;
9.40 val {scr = Prog sc,... } = MethodC.from_store ["diff", "integration", "named"];
9.41 val [_,_, F2_] = formal_args sc;
9.42 if F1_ = F2_ then () else error "integrate.sml: unequal find's";
9.43
9.44 -val ((dsc as Const ("Integrate.antiDerivativeName", _))
9.45 +val ((dsc as Const (\<^const_name>\<open>antiDerivativeName\<close>, _))
9.46 $ Free ("ff", F3_type)) = str2t "antiDerivativeName ff";
9.47 if Input_Descript.is_a dsc then () else error "integrate.sml: no description";
9.48 if F1_type = F3_type then ()
9.49 @@ -371,7 +371,7 @@
9.50
9.51 Test_Tool.show_ptyps();
9.52 val pbl = Problem.from_store ["integrate", "function"];
9.53 -case #cas pbl of SOME (Const ("Integrate.Integrate",_) $ _) => ()
9.54 +case #cas pbl of SOME (Const (\<^const_name>\<open>Integrate\<close>,_) $ _) => ()
9.55 | _ => error "integrate.sml: Integrate.Integrate ???";
9.56
9.57
10.1 --- a/test/Tools/isac/Knowledge/poly-1.sml Mon Jul 19 15:34:54 2021 +0200
10.2 +++ b/test/Tools/isac/Knowledge/poly-1.sml Mon Jul 19 17:29:35 2021 +0200
10.3 @@ -151,7 +151,7 @@
10.4 val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
10.5 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed";
10.6
10.7 -(*. . . . . . . . . . . . the same with Const ("Partial_Functions.AA", _) . . . . . . . . . . . *)
10.8 +(*. . . . . . . . . . . . the same with Const (\<^const_name>\<open>AA\<close>, _) . . . . . . . . . . . *)
10.9 val thy = @{theory Partial_Fractions}
10.10 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
10.11
10.12 @@ -193,27 +193,27 @@
10.13 val ll = map monom2list (poly2list t);
10.14
10.15 (*+*)UnparseC.terms (poly2list t) = "[\"(3::'a) * b\", \"a * (2::'a)\"]";
10.16 -(*+*)val [ [(Const ("Num.numeral_class.numeral", _) $ _), Free ("b", _)],
10.17 -(*+*) [Free ("a", _), (Const ("Num.numeral_class.numeral", _) $ _)]
10.18 +(*+*)val [ [(Const (\<^const_name>\<open>numeral\<close>, _) $ _), Free ("b", _)],
10.19 +(*+*) [Free ("a", _), (Const (\<^const_name>\<open>numeral\<close>, _) $ _)]
10.20 (*+*) ] = map monom2list (poly2list t);
10.21
10.22 val lls = map sort_varList ll;
10.23
10.24 (*+*)case map sort_varList ll of
10.25 -(*+*) [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("b", _)],
10.26 -(*+*) [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)]
10.27 +(*+*) [ [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("b", _)],
10.28 +(*+*) [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("a", _)]
10.29 (*+*) ] => ()
10.30 (*+*)| _ => error "map sort_varList CHANGED";
10.31
10.32 val T = type_of t;
10.33 val ls = map (create_monom T) lls;
10.34
10.35 -(*+*)val [Const ("Groups.times_class.times", _) $ _ $ Free ("b", _),
10.36 -(*+*) Const ("Groups.times_class.times", _) $ _ $ Free ("a", _)] = map (create_monom T) lls;
10.37 +(*+*)val [Const (\<^const_name>\<open>times\<close>, _) $ _ $ Free ("b", _),
10.38 +(*+*) Const (\<^const_name>\<open>times\<close>, _) $ _ $ Free ("a", _)] = map (create_monom T) lls;
10.39
10.40 (*+*)case map (create_monom T) lls of
10.41 -(*+*) [Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("b", _),
10.42 -(*+*) Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("a", _)
10.43 +(*+*) [Const (\<^const_name>\<open>times\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ _) $ Free ("b", _),
10.44 +(*+*) Const (\<^const_name>\<open>times\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ _) $ Free ("a", _)
10.45 (*+*) ] => ()
10.46 (*+*)| _ => error "map (create_monom T) CHANGED";
10.47
10.48 @@ -232,15 +232,15 @@
10.49 "~~~~~~~ fun sort_variables , args:"; val (t) = (t);
10.50 val ll = map monom2list (poly2list t);
10.51
10.52 -(*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)],
10.53 -(*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*already correct order*)
10.54 +(*+*)val [ [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("a", _)],
10.55 +(*+*) [Const (\<^const_name>\<open>uminus\<close>, _) $ _, Free ("a", _)] (*already correct order*)
10.56 (*+*) ] = map monom2list (poly2list t);
10.57
10.58 val lls = map
10.59 sort_varList ll;
10.60
10.61 -(*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)],
10.62 -(*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*ERROR: NO swap here*)
10.63 +(*+*)val [ [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("a", _)],
10.64 +(*+*) [Const (\<^const_name>\<open>uminus\<close>, _) $ _, Free ("a", _)] (*ERROR: NO swap here*)
10.65 (*+*) ] = map sort_varList ll;
10.66
10.67 map sort_varList ll;
10.68 @@ -362,7 +362,7 @@
10.69 "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee1);
10.70 "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
10.71 (*if*) (is_nums x) (*else*);
10.72 - val (Const ("Transcendental.powr", _) $ Free _ $ t) =
10.73 + val (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ t) =
10.74 (*case*) x (*of*);
10.75 (*+*)UnparseC.term x = "x \<up> 2";
10.76 (*if*) TermC.is_num t (*then*);
10.77 @@ -370,7 +370,7 @@
10.78 counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
10.79 "~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
10.80 (*if*) (is_nums x) (*else*);
10.81 - val (Const ("Transcendental.powr", _) $ Free _ $ t) =
10.82 + val (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ t) =
10.83 (*case*) x (*of*);
10.84 (*+*)UnparseC.term x = "y \<up> 2";
10.85 (*if*) TermC.is_num t (*then*);
10.86 @@ -385,7 +385,7 @@
10.87 "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee2);
10.88 "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
10.89 (*if*) (is_nums x) (*else*);
10.90 -val (Const ("Transcendental.powr", _) $ Free _ $ t) =
10.91 +val (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ t) =
10.92 (*case*) x (*of*);
10.93 (*+*)UnparseC.term x = "x \<up> 3";
10.94 (*if*) TermC.is_num t (*then*);
10.95 @@ -468,10 +468,10 @@
10.96 "----- eval_is_multUnordered ---";
10.97 val tm = TermC.str2term "(5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (- 1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + - 1 * (3 * x \<up> 5 * - 1) + (-48 * x \<up> 4 + 8))) is_multUnordered";
10.98 case eval_is_multUnordered "testid" "" tm thy of
10.99 - SOME (_, Const ("HOL.Trueprop", _) $
10.100 - (Const ("HOL.eq", _) $
10.101 - (Const ("Poly.is_multUnordered", _) $ _) $
10.102 - Const ("HOL.True", _))) => ()
10.103 + SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $
10.104 + (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
10.105 + (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $
10.106 + Const (\<^const_name>\<open>True\<close>, _))) => ()
10.107 | _ => error "poly.sml diff. eval_is_multUnordered";
10.108
10.109 "----- rewrite_set_ STILL DIDN'T WORK";
10.110 @@ -492,9 +492,9 @@
10.111 case eval_is_multUnordered "xxx " "yyy " t thy of
10.112 SOME
10.113 ("xxx 3 * a + - 2 * a_",
10.114 - Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
10.115 - Const ("HOL.False", _))) => ()
10.116 -(* Const ("HOL.True", _))) => () <<<<<--------------------------- this is false*)
10.117 + Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
10.118 + Const (\<^const_name>\<open>False\<close>, _))) => ()
10.119 +(* Const (\<^const_name>\<open>True\<close>, _))) => () <<<<<--------------------------- this is false*)
10.120 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
10.121
10.122 "----- is_multUnordered --- (- 2 * a) is_multUnordered = False";
10.123 @@ -507,8 +507,8 @@
10.124 case eval_is_multUnordered "xxx " "yyy " t thy of
10.125 SOME
10.126 ("xxx - 2 * a_",
10.127 - Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
10.128 - Const ("HOL.False", _))) => ()
10.129 + Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
10.130 + Const (\<^const_name>\<open>False\<close>, _))) => ()
10.131 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
10.132
10.133 "----- is_multUnordered --- (a) is_multUnordered = False";
10.134 @@ -521,8 +521,8 @@
10.135 case eval_is_multUnordered "xxx " "yyy " t thy of
10.136 SOME
10.137 ("xxx a_",
10.138 - Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
10.139 - Const ("HOL.False", _))) => ()
10.140 + Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
10.141 + Const (\<^const_name>\<open>False\<close>, _))) => ()
10.142 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
10.143
10.144 "----- is_multUnordered --- (- 2) is_multUnordered = False";
10.145 @@ -535,8 +535,8 @@
10.146 case eval_is_multUnordered "xxx " "yyy " t thy of
10.147 SOME
10.148 ("xxx - 2_",
10.149 - Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
10.150 - Const ("HOL.False", _))) => ()
10.151 + Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
10.152 + Const (\<^const_name>\<open>False\<close>, _))) => ()
10.153 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
10.154
10.155
10.156 @@ -642,10 +642,10 @@
10.157 ((is_polyexp t) andalso not (t = sort_variables t)) = true; (*isa == isa2*)
10.158
10.159 (*+*)if is_polyexp t then () else error "is_polyexp a \<up> 2 * b CHANGED";
10.160 -"~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (t);
10.161 +"~~~~~ fun is_polyexp , args:"; val (Const (\<^const_name>\<open>times\<close>,_) $ num $ Free _) = (t);
10.162 (*if*) TermC.is_num num (*else*);
10.163
10.164 -"~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (num);
10.165 +"~~~~~ fun is_polyexp , args:"; val (Const (\<^const_name>\<open>times\<close>,_) $ num $ Free _) = (num);
10.166 (*if*) TermC.is_num num (*else*);
10.167 (*if*) TermC.is_variable num (*then*);
10.168
10.169 @@ -678,7 +678,7 @@
10.170 (*+*)else error "6 * a is_multUnordered = False CHANGED";
10.171
10.172 "~~~~~ fun eval_is_multUnordered , args:"; val ((thmid:string), _,
10.173 - (t as (Const("Poly.is_multUnordered", _) $ arg)), thy) = ("xxx", (), t, @{theory});
10.174 + (t as (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ arg)), thy) = ("xxx", (), t, @{theory});
10.175 (*if*) is_multUnordered arg (*else*);
10.176
10.177 "~~~~~ fun is_multUnordered , args:"; val (t) = (arg);
11.1 --- a/test/Tools/isac/Knowledge/poly-2.sml Mon Jul 19 15:34:54 2021 +0200
11.2 +++ b/test/Tools/isac/Knowledge/poly-2.sml Mon Jul 19 17:29:35 2021 +0200
11.3 @@ -126,10 +126,10 @@
11.4 "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
11.5 val thy = @{theory Partial_Fractions}
11.6 val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
11.7 -val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
11.8 +val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
11.9
11.10 val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
11.11 -val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
11.12 +val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
11.13
11.14 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
11.15 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
11.16 @@ -199,7 +199,7 @@
11.17 ***
11.18 *)
11.19 case t of
11.20 - Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.one_class.one", _) => ()
11.21 + Const (\<^const_name>\<open>uminus\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _) => ()
11.22 | _ => error "internal representation of \"- 1\" changed";
11.23
11.24 "======= these external values all have the same internal representation";
11.25 @@ -259,7 +259,7 @@
11.26
11.27 eval_is_addUnordered "xxx" "yyy" t @{theory};
11.28 "~~~~~ fun eval_is_addUnordered , args:"; val ((thmid:string), _,
11.29 - (t as (Const("Poly.is_addUnordered", _) $ arg)), thy) =
11.30 + (t as (Const (\<^const_name>\<open>is_addUnordered\<close>, _) $ arg)), thy) =
11.31 ("xxx", "yyy", t, @{theory});
11.32
11.33 (*if*) is_addUnordered arg;
12.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Mon Jul 19 15:34:54 2021 +0200
12.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Mon Jul 19 17:29:35 2021 +0200
12.3 @@ -95,15 +95,15 @@
12.4 val t = TermC.str2term "12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * (g::real)";
12.5 val SOME ("12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g = True", _) =
12.6 eval_kleiner "aaa" "bbb" t "ccc";
12.7 -"~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const ("PolyMinus.kleiner",_) $ a $ b)), _) =
12.8 +"~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const (\<^const_name>\<open>kleiner\<close>",_) $ a $ b)), _) =
12.9 ("aaa", "bbb", t, "ccc");
12.10 (*if*) TermC.is_num b (*else*);
12.11
12.12 (*if*) identifier a < identifier b (*else*);
12.13 "~~~~~ fun identifier , args:"; val (t) = (a);
12.14 (*+*)case a of
12.15 - Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $
12.16 - (Const ("Num.num.Bit0", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _)))) => ()
12.17 + Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $
12.18 + (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
12.19 | _ => error "eval_kleiner CHANGED"; (*isa*)
12.20 ( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
12.21
13.1 --- a/test/Tools/isac/Knowledge/rateq.sml Mon Jul 19 15:34:54 2021 +0200
13.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Mon Jul 19 17:29:35 2021 +0200
13.3 @@ -110,19 +110,19 @@
13.4 (thy, ptp, sc, E, l, true, a, v);
13.5 1 < length l; (*true*)
13.6 val up = drop_last l;
13.7 -TermC.sub_at up sc; (* = Const ("HOL.Let", *)
13.8 +TermC.sub_at up sc; (* = Const (\<^const_name>\<open>Let\<close>, *)
13.9 "~~~~~ fun scan_up, args:"; val (thy, ptp, (scr as (Prog sc)), E, l, ay,
13.10 - (t as Const ("HOL.Let",_) $ _), a, v) = (thy, ptp, (Prog sc), E, up, ay, (TermC.sub_at up sc), a, v);
13.11 + (t as Const (\<^const_name>\<open>Let\<close>,_) $ _), a, v) = (thy, ptp, (Prog sc), E, up, ay, (TermC.sub_at up sc), a, v);
13.12 ay = Napp_; (*false*)
13.13 val up = drop_last l;
13.14 -val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = TermC.sub_at up sc; (*Const ("Prog_Tac.SubProblem",..*)
13.15 +val (Const (\<^const_name>\<open>Let\<close>,_) $ e $ (Abs (i,T,body))) = TermC.sub_at up sc; (*Const (\<^const_name>\<open>SubProblem\<close>,..*)
13.16 val i = mk_Free (i, T);
13.17 val E = Env.update E (i, v);
13.18 "~~~~~ fun scan_dn, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v) =
13.19 (thy, ptp, E, (up@[R,D]), body, a, v);
13.20 "~~~~~ fun check_leaf, args:"; val (call, thy, srls, (E, (a, v)), t) = ("next ", th, sr, (E, (a, v)), t);
13.21 "~~~~~ fun eval_leaf, args:"; val (E, a, v,
13.22 - (t as (Const ("Prog_Tac.Check_elementwise",_) $ _ $ _ ))) = (E, a, v, t);
13.23 + (t as (Const (\<^const_name>\<open>Check_elementwise\<close>,_) $ _ $ _ ))) = (E, a, v, t);
13.24 val Program.Tac tm = Program.Tac (subst_atomic E t);
13.25 UnparseC.term tm = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
13.26 (* ------ \<up> ----- ? "x" ?*)
14.1 --- a/test/Tools/isac/Knowledge/rational-1.sml Mon Jul 19 15:34:54 2021 +0200
14.2 +++ b/test/Tools/isac/Knowledge/rational-1.sml Mon Jul 19 17:29:35 2021 +0200
14.3 @@ -40,12 +40,12 @@
14.4 (vs, (TermC.str2term "12 * x \<up> 3"));
14.5
14.6 monom_of_term vs (1, replicate (length vs) 0) t;(*poly malformed 1 with x \<up> 3*)
14.7 -"~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const ("Groups.times_class.times", _) $ m1 $ m2)) =
14.8 +"~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (\<^const_name>\<open>times\<close>, _) $ m1 $ m2)) =
14.9 (vs, (1, replicate (length vs) 0), t);
14.10 val (c', es') =
14.11
14.12 monom_of_term vs (c, es) m1;
14.13 -"~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const ("Transcendental.powr", _) $ (t as Free _) $ (Const ("Num.numeral_class.numeral", _) $ num)) ) =
14.14 +"~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (\<^const_name>\<open>powr\<close>, _) $ (t as Free _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ num)) ) =
14.15 (vs, (c', es'), m2);
14.16 (*+*)c = 12;
14.17 (*+*)(num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = [3, 0, 0];
15.1 --- a/test/Tools/isac/Knowledge/rational-2.sml Mon Jul 19 15:34:54 2021 +0200
15.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml Mon Jul 19 17:29:35 2021 +0200
15.3 @@ -453,7 +453,7 @@
15.4
15.5 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (id, _))) =
15.6 (vs, (1, replicate (length vs) 0), t);
15.7 -case vs of [Const ("Partial_Fractions.AA", _), Const ("Partial_Fractions.BB", _)] =>
15.8 +case vs of [Const (\<^const_name>\<open>AA\<close>, _), Const (\<^const_name>\<open>BB\<close>, _)] =>
15.9 if c = 1 andalso id = "Partial_Fractions.AA"
15.10 then () else error "monom_of_term Const changed 1"
15.11 | _ => error "monom_of_term Const changed 2";
15.12 @@ -463,12 +463,12 @@
15.13 "----------- fun cancel_p with Const AA --------------------------------------------------------";
15.14 val thy = @{theory Partial_Fractions};
15.15 val ctxt = Proof_Context.init_global @{theory}
15.16 -val SOME t = TermC.parseNEW ctxt "2 * AA / 2"; (* Const ("Free ("AA", "real") *)
15.17 +val SOME t = TermC.parseNEW ctxt "2 * AA / 2"; (* Const (\<^const_name>\<open>AA\<close>, "real") *)
15.18
15.19 val SOME (t', _) = rewrite_set_ thy true cancel_p t;
15.20 case t' of
15.21 - Const ("Rings.divide_class.divide", _) $ Const ("Partial_Fractions.AA", _) $
15.22 - Const ("Groups.one_class.one", _) => ()
15.23 + Const (\<^const_name>\<open>divide\<close>, _) $ Const (\<^const_name>\<open>AA\<close>, _) $
15.24 + Const (\<^const_name>\<open>one_class.one\<close>, _) => ()
15.25 | _ => error "WRONG rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA changed";
15.26
15.27 "~~~~~ fun cancel_p , args:"; val (t) = (t);
15.28 @@ -479,7 +479,7 @@
15.29 then () else error "check_fraction (2 * AA / 2) changed";
15.30 val vs = TermC.vars_of t;
15.31 case vs of
15.32 - [Const ("Partial_Fractions.AA", _)] => ()
15.33 + [Const (\<^const_name>\<open>AA\<close>, _)] => ()
15.34 | _ => error "rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA/1 changed";
15.35
15.36
16.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Mon Jul 19 15:34:54 2021 +0200
16.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Mon Jul 19 17:29:35 2021 +0200
16.3 @@ -115,11 +115,11 @@
16.4 val (_ $ v) = t;
16.5 TermC.is_list v;
16.6 pbl_ids ctxt d v;
16.7 -[Const ("List.list.Cons", "[bool, bool List.list] => bool List.list") $
16.8 - (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil", "bool List..
16.9 +[Const (\<^const_name>\<open>Cons\<close>, "[bool, bool List.list] => bool List.list") $
16.10 + (Const # $ Free # $ Const (#,#)) $ Const (\<^const_name>\<open>Nil\<close>, "bool List..
16.11
16.12 val (dsc,vl) = (Input_Descript.split o Thm.term_of o the o (TermC.parse thy)) "solveFor x";
16.13 -val dsc = Const ("Input_Descript.solveFor", "RealDef.real => Tools.una") : term
16.14 +val dsc = Const (\<^const_name>\<open>Input_Descript.solveFor\<close>, "RealDef.real => Tools.una") : term
16.15 val vl = Free ("x", "RealDef.real") : term
16.16
16.17 val (dsc,id) = (split_did o Thm.term_of o the o (TermC.parse thy)) "solveFor v_";
17.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Mon Jul 19 15:34:54 2021 +0200
17.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Mon Jul 19 17:29:35 2021 +0200
17.3 @@ -232,7 +232,7 @@
17.4 (Logic.count_prems r', [], r'));
17.5 case p' of
17.6 [Const (\<^const_name>\<open>Not\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _)
17.7 - $ Free ("x", _) $ Const ("Groups.zero_class.zero", _))] => ()
17.8 + $ Free ("x", _) $ Const (\<^const_name>\<open>zero_class.zero\<close>, _))] => ()
17.9 | _ => error "rewrite.sml assumption changed";
17.10 "===== \<up> make asms without Trueprop --- \<up> ";
17.11 "----- step 4: get the (instantiated) RHS";
17.12 @@ -377,12 +377,12 @@
17.13 (*+*)case eval_is_multUnordered "testid" "" tm thy of
17.14 (*+*) SOME
17.15 (*+*) ("testidx \<up> 2 * x_",
17.16 -(*+*) Const ("HOL.Trueprop", _) $
17.17 -(*+*) (Const ("HOL.eq", _) $
17.18 -(*+*) (Const ("Poly.is_multUnordered", _) $
17.19 -(*+*) (Const ("Groups.times_class.times", _) $
17.20 -(*+*) (Const ("Transcendental.powr", _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $
17.21 -(*+*) Const ("HOL.True", _))) => ()
17.22 +(*+*) Const (\<^const_name>\<open>Trueprop\<close>, _) $
17.23 +(*+*) (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
17.24 +(*+*) (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $
17.25 +(*+*) (Const (\<^const_name>\<open>times\<close>, _) $
17.26 +(*+*) (Const (\<^const_name>\<open>powr\<close>, _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $
17.27 +(*+*) Const (\<^const_name>\<open>True\<close>, _))) => ()
17.28 (*+*)(* ^^^^^^ compare ---vvv *)
17.29 (*+*)| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED";
17.30
17.31 @@ -392,7 +392,7 @@
17.32 case eval_is_multUnordered "testid" "" tm thy of
17.33 SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $
17.34 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
17.35 - (Const ("Poly.is_multUnordered", _) $ _) $
17.36 + (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $
17.37 Const (\<^const_name>\<open>True\<close>, _))) => ()
17.38 | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
17.39
18.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Mon Jul 19 15:34:54 2021 +0200
18.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Mon Jul 19 17:29:35 2021 +0200
18.3 @@ -35,11 +35,11 @@
18.4 (* ERROR Specify.item_to_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt
18.5 IN Minimsubpbl/150-add-given.sml IS CAUSED HEREBY:*)
18.6 case oris of
18.7 - [(1, [1], "#Given", Const ("Input_Descript.equality", _),
18.8 - [Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $ Const ("Partial_Fractions.AA", _) $ Const ("Groups.one_class.one", _)) $
18.9 - (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ Const ("Num.num.One", _)))]),
18.10 - (2, [1], "#Given", Const ("Input_Descript.solveFor", _), [Const ("Partial_Fractions.AA", _)]),
18.11 - (3, [1], "#Find", Const ("Input_Descript.solutions", _), [Free ("L", _)])] => ()
18.12 + [(1, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.equality\<close>, _),
18.13 + [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>plus_class.plus\<close>, _) $ Const (\<^const_name>\<open>AA\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _)) $
18.14 + (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))]),
18.15 + (2, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.solveFor\<close>, _), [Const (\<^const_name>\<open>AA\<close>, _)]),
18.16 + (3, [1], "#Find", Const (\<^const_name>\<open>Input_Descript.solutions\<close>, _), [Free ("L", _)])] => ()
18.17 | ((1, [1], "#undef", Const ("empty", _), _) :: _) => error "START specify: oris are not properly initialised"
18.18 | _ => error ""
18.19
18.20 @@ -51,11 +51,11 @@
18.21 val oris = O_Model.init fmz thy yyy
18.22 ;
18.23 case oris of
18.24 - [(1, [1], "#Given", Const ("Input_Descript.equality", _),
18.25 - [Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $ Const ("Partial_Fractions.AA", _) $ Const ("Groups.one_class.one", _)) $
18.26 - (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ Const ("Num.num.One", _)))]),
18.27 - (2, [1], "#Given", Const ("Input_Descript.solveFor", _), [Const ("Partial_Fractions.AA", _)]),
18.28 - (3, [1], "#Find", Const ("Input_Descript.solutions", _), [Free ("L", _)])] => ()
18.29 + [(1, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.equality\<close>, _),
18.30 + [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>plus_class.plus\<close>, _) $ Const (\<^const_name>\<open>AA\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _)) $
18.31 + (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))]),
18.32 + (2, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.solveFor\<close>, _), [Const (\<^const_name>\<open>AA\<close>, _)]),
18.33 + (3, [1], "#Find", Const (\<^const_name>\<open>Input_Descript.solutions\<close>, _), [Free ("L", _)])] => ()
18.34 | ((1, [1], "#undef", Const ("empty", _), _) :: _) => error "START specify: oris are not properly initialised"
18.35 | _ => error ""
18.36
18.37 @@ -63,12 +63,12 @@
18.38 val ctxt = ContextC.initialise' thy fmz;
18.39 (*ADD check*)
18.40 case TermC.parseNEW ctxt "equality (x+1=(2::real))" of
18.41 - SOME (Const ("Input_Descript.equality", _) $
18.42 - (Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $ Free ("x", _) $ Const ("Groups.one_class.one", _)) $
18.43 - (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ Const ("Num.num.One", _))))
18.44 + SOME (Const (\<^const_name>\<open>Input_Descript.equality\<close>, _) $
18.45 + (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>plus_class.plus\<close>, _) $ Free ("x", _) $ Const (\<^const_name>\<open>one_class.one\<close>, _)) $
18.46 + (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))))
18.47 ) => ()
18.48 | SOME (Free ("equality", _) $
18.49 - (Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $
18.50 + (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>plus_class.plus\<close>, _) $
18.51 Free ("x", _) $ Free ("1", _)) $ Free ("2", _))) => error "xxx"
18.52 | _ => error "something is wrong with initialising Minisubpnl";
18.53
19.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Mon Jul 19 15:34:54 2021 +0200
19.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Mon Jul 19 17:29:35 2021 +0200
19.3 @@ -57,12 +57,12 @@
19.4
19.5 val Accept_Tac1 (_, _, Rewrite_Set' (_, _, Rule_Set.Repeat {id = "norm_equation", ...}, _, _)) = (*case*)
19.6 scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
19.7 -"~~~~~ fun scan_dn1, args:"; val ((xxx as (cstate, _, _)), ist, (Const ("Tactical.Chain"(*1*),_) $e1 $ e2 $ a)) =
19.8 +"~~~~~ fun scan_dn1, args:"; val ((xxx as (cstate, _, _)), ist, (Const (\<^const_name>\<open>Chain\<close>(*1*),_) $e1 $ e2 $ a)) =
19.9 (xxx, (ist |> path_down [L, R]), e);
19.10
19.11 val Accept_Tac1 _ = (*case*)
19.12 scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
19.13 -"~~~~~ fun scan_dn1, args:"; val (xxx, ist, (Const ("Tactical.Try"(*1*),_) $ e)) =
19.14 +"~~~~~ fun scan_dn1, args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*1*),_) $ e)) =
19.15 (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
19.16
19.17 (*+*)UnparseC.term e1 = "Try (Rewrite_Set ''norm_equation'')" (*in isabisac*);
19.18 @@ -76,7 +76,7 @@
19.19 val Associated (Rewrite_Set' _, _, _) = (*case*)
19.20 associate pt ctxt (m, stac) (*of*);
19.21 "~~~~~ fun associate, args:"; val (_, ctxt, (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _))),
19.22 - (Const ("Prog_Tac.Rewrite_Set", _) $ rls_ $ f_)) = (pt, ctxt, m, stac);
19.23 + (Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ rls_ $ f_)) = (pt, ctxt, m, stac);
19.24
19.25 (*+*)if Rule_Set.id rls = HOLogic.dest_string rls_ then () else error "Prog_Tac.associate changed";
19.26
19.27 @@ -114,7 +114,7 @@
19.28 (*if*) 1 < length path (*then*);
19.29
19.30 scan_up yyy (ist |> path_up) (go_up path prog);
19.31 -"~~~~~ fun scan_up , args:"; val (yyy, ist, (Const ("Tactical.Try"(*2*), _) $ _)) =
19.32 +"~~~~~ fun scan_up , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ _)) =
19.33 (yyy, (ist |> path_up), (go_up path prog));
19.34 (*\------------------- end step into 1 -----------------------------------------------------/*)
19.35
19.36 @@ -165,7 +165,7 @@
19.37 (*if*) 1 < length path (*then*);
19.38
19.39 scan_up yyy (ist |> path_up) (go_up path prog);
19.40 -"~~~~~ and scan_up , args:"; val (yyy, ist, (Const ("Tactical.Try"(*1*),_) $ _ ))
19.41 +"~~~~~ and scan_up , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Try\<close>(*1*),_) $ _ ))
19.42 = (yyy, (ist |> path_up), (go_up path prog));
19.43
19.44 go_scan_up yyy (ist |> set_found);
19.45 @@ -174,7 +174,7 @@
19.46 (*if*) 1 < length path (*then*);
19.47
19.48 scan_up yyy (ist |> path_up) (go_up path prog);
19.49 -"~~~~~ and scan_up , args:"; val (yyy, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
19.50 +"~~~~~ and scan_up , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ _ $ _))
19.51 = (yyy, (ist |> path_up), (go_up path prog));
19.52
19.53 go_scan_up yyy ist;
19.54 @@ -183,7 +183,7 @@
19.55 (*if*) 1 < length path (*then*);
19.56
19.57 scan_up yyy (ist |> path_up) (go_up path prog);
19.58 -"~~~~~ fun scan_up , args:"; val (yyy, ist, (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _))
19.59 +"~~~~~ fun scan_up , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Chain\<close>(*1*), _) $ _ $ _ $ _))
19.60 = (yyy, (ist |> path_up), (go_up path prog));
19.61
19.62 go_scan_up yyy ist;
19.63 @@ -210,7 +210,7 @@
19.64
19.65 (*val m =*)
19.66 Sub_Problem.tac_from_prog pt stac;
19.67 -"~~~~~ fun tac_from_prog , args:"; val (pt, _, (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags'))
19.68 +"~~~~~ fun tac_from_prog , args:"; val (pt, _, (stac as Const (\<^const_name>\<open>SubProblem\<close>, _) $ spec' $ ags'))
19.69 = (pt, (Proof_Context.theory_of ctxt), stac);
19.70 val (dI, pI, mI) = Prog_Tac.dest_spec spec'
19.71 val thy = ThyC.sub_common (ThyC.get_theory dI, rootthy pt);
20.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Mon Jul 19 15:34:54 2021 +0200
20.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Mon Jul 19 17:29:35 2021 +0200
20.3 @@ -58,7 +58,7 @@
20.4 (*if*) 1 < length path (*true*);
20.5
20.6 scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
20.7 -"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const ("Tactical.Try"(*2*), _) $ _))
20.8 +"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ _))
20.9 = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
20.10
20.11 go_scan_up1 pcct ist;
20.12 @@ -67,7 +67,7 @@
20.13 (*if*) 1 < length path (*true*);
20.14
20.15 scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
20.16 -"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
20.17 +"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ _ $ _))
20.18 = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
20.19
20.20 go_scan_up1 pcct ist (*2*: comes from e2*);
20.21 @@ -76,7 +76,7 @@
20.22 (*if*) 1 < length path (*true*);
20.23
20.24 scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
20.25 -"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _))
20.26 +"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const (\<^const_name>\<open>Chain\<close>(*1*), _) $ _ $ _ $ _))
20.27 = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
20.28
20.29 go_scan_up1 pcct ist (*all has been done in (*2*) below*);
20.30 @@ -104,7 +104,7 @@
20.31 = ("locate", ctxt, eval, (get_subst ist), t);
20.32
20.33 val (Program.Tac stac, a) = (*case*) Prog_Tac.eval_leaf E a v t (*of*);
20.34 -"~~~~~ fun eval_leaf , args:"; val (E, _, _, (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)))
20.35 +"~~~~~ fun eval_leaf , args:"; val (E, _, _, (t as (Const (\<^const_name>\<open>SubProblem\<close>, _) $ _ $ _)))
20.36 = (E, a, v, t);
20.37
20.38 (Program.Tac (subst_atomic E t), NONE); (*return value*)
21.1 --- a/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Mon Jul 19 15:34:54 2021 +0200
21.2 +++ b/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Mon Jul 19 17:29:35 2021 +0200
21.3 @@ -71,7 +71,7 @@
21.4 (*if*) 1 < length path (*then*);
21.5
21.6 scan_up pcc (ist |> path_up) (go_up path sc);
21.7 -"~~~~~ and scan_up , args:"; val (pcc, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
21.8 +"~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ _ $ _))
21.9 = (pcc, (ist |> path_up), (go_up path sc));
21.10
21.11 go_scan_up pcc ist;
21.12 @@ -80,11 +80,11 @@
21.13 (*if*) 1 < length path (*then*);
21.14
21.15 scan_up pcc (ist |> path_up) (go_up path sc);
21.16 -"~~~~~ and scan_up , args:"; val ((pcc as (_, cc)), ist, (Const ("Tactical.Repeat"(*2*), _) $ e))
21.17 +"~~~~~ and scan_up , args:"; val ((pcc as (_, cc)), ist, (Const (\<^const_name>\<open>Repeat\<close>(*2*), _) $ e))
21.18 = (pcc, (ist |> path_up), (go_up path sc));
21.19
21.20 (*case*) scan_dn cc (ist |> path_down [R]) e (*of*);
21.21 -"~~~~~ fun scan_dn , args:"; val (pcc, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
21.22 +"~~~~~ fun scan_dn , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ _ $ _))
21.23 = (cc, (ist |> path_down [R]), e);
21.24 (*============== stopped, when all worked ===================*)
21.25
22.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Mon Jul 19 15:34:54 2021 +0200
22.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Mon Jul 19 17:29:35 2021 +0200
22.3 @@ -89,7 +89,7 @@
22.4
22.5 val Check_elementwise "Assumptions" =
22.6 LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) stac;
22.7 -"~~~~~ fun tac_from_prog , args:"; val (pt, thy, (Const("Prog_Tac.Check_elementwise",_) $ _ $
22.8 +"~~~~~ fun tac_from_prog , args:"; val (pt, thy, (Const (\<^const_name>\<open>Check_elementwise\<close>, _) $ _ $
22.9 (set as Const (\<^const_name>\<open>Collect\<close>,_) $ Abs (_,_,pred))))
22.10 = (pt, (Proof_Context.theory_of ctxt), stac);
22.11
23.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Mon Jul 19 15:34:54 2021 +0200
23.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Mon Jul 19 17:29:35 2021 +0200
23.3 @@ -257,9 +257,9 @@
23.4 if UnparseC.term t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''))" then ()
23.5 else error "rule2stac_inst Thm.. changed";
23.6 case t of
23.7 - (Const ("Tactical.Try", _) $
23.8 - (Const ("Tactical.Repeat", _) $
23.9 - (Const ("Prog_Tac.Rewrite_Inst", _) $
23.10 + (Const (\<^const_name>\<open>Try\<close>, _) $
23.11 + (Const (\<^const_name>\<open>Repeat\<close>, _) $
23.12 + (Const (\<^const_name>\<open>Rewrite_Inst\<close>, _) $
23.13 (Const (\<^const_name>\<open>Cons\<close>, _) $
23.14 (Const (\<^const_name>\<open>Pair\<close>, _) $
23.15 bdv $
23.16 @@ -277,12 +277,12 @@
23.17 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
23.18 val {scr, ...} = MethodC.from_store ["Test", "sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
23.19 case stacpbls sc of
23.20 - [Const ("Prog_Tac.Rewrite", _) $ square_equation_left,
23.21 - Const ("Prog_Tac.Rewrite_Set", _) $ Test_simplify,
23.22 - Const ("Prog_Tac.Rewrite_Set", _) $ rearrange_assoc,
23.23 - Const ("Prog_Tac.Rewrite_Set", _) $ isolate_root,
23.24 - Const ("Prog_Tac.Rewrite_Set", _) $ norm_equation,
23.25 - Const ("Prog_Tac.Rewrite_Set_Inst", _) $
23.26 + [Const (\<^const_name>\<open>Rewrite\<close>, _) $ square_equation_left,
23.27 + Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ Test_simplify,
23.28 + Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ rearrange_assoc,
23.29 + Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ isolate_root,
23.30 + Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ norm_equation,
23.31 + Const (\<^const_name>\<open>Rewrite_Set_Inst\<close>, _) $
23.32 (Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ bdv $ Free ("v_v", _)) $
23.33 Const (\<^const_name>\<open>Nil\<close>, _)) $ isolate_bdv] =>
23.34 if HOLogic.dest_string square_equation_left = "square_equation_left" andalso
24.1 --- a/test/Tools/isac/ProgLang/calculate.sml Mon Jul 19 15:34:54 2021 +0200
24.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Mon Jul 19 17:29:35 2021 +0200
24.3 @@ -30,9 +30,9 @@
24.4 case xxx of
24.5 SOME
24.6 ("#: (3::'a) + 2 = (5::'a)",
24.7 - Const ("HOL.Trueprop", _) $
24.8 - (Const ("HOL.eq", _) $
24.9 - (Const ("Groups.plus_class.plus", _) $ _ $
24.10 - (Const ("Num.numeral_class.numeral", _) $ _ )) $
24.11 + Const (\<^const_name>\<open>Trueprop\<close>, _) $
24.12 + (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
24.13 + (Const (\<^const_name>\<open>plus_class.plus\<close>, _) $ _ $
24.14 + (Const (\<^const_name>\<open>numeral\<close>, _) $ _ )) $
24.15 _ )) => ()
24.16 | _ => error "eval_binop #: (3::'a) + 2 = (5::'a) CHANGED"
25.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Mon Jul 19 15:34:54 2021 +0200
25.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Mon Jul 19 17:29:35 2021 +0200
25.3 @@ -280,8 +280,8 @@
25.4
25.5 case (op_, t) of
25.6 ("Transcendental.powr",
25.7 - Const ("Transcendental.powr", _) $ (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _))) $
25.8 - (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ Const ("Num.num.One", _)))) => ()
25.9 + Const (\<^const_name>\<open>powr\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $
25.10 + (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
25.11 | _ => error "3 \<up> 2 CHANGED";
25.12 val SOME (id, t') = eval_binop thmid op_ t thy;
25.13 (*** calc: operator = pow not defined*)
25.14 @@ -303,8 +303,8 @@
25.15 val (t1, t2) = (@{term 3}, @{term "2::real"});
25.16
25.17 "~~~~~ fun calcul , args:"; val (op_, (t1, t2)) = ("Groups.plus_class.plus", (t1, t2));
25.18 - val (Const ("Num.numeral_class.numeral", _) $ n1) = t1;
25.19 - val (Const ("Num.numeral_class.numeral", _) $ n2) = t2;
25.20 + val (Const (\<^const_name>\<open>numeral\<close>, _) $ n1) = t1;
25.21 + val (Const (\<^const_name>\<open>numeral\<close>, _) $ n2) = t2;
25.22 val (T, _) = HOLogic.dest_number t1
25.23 val (i1, i2) = (HOLogic.dest_numeral n1, HOLogic.dest_numeral n2)
25.24 val result =
26.1 --- a/test/Tools/isac/ProgLang/listC.sml Mon Jul 19 15:34:54 2021 +0200
26.2 +++ b/test/Tools/isac/ProgLang/listC.sml Mon Jul 19 17:29:35 2021 +0200
26.3 @@ -56,12 +56,12 @@
26.4
26.5 val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
26.6 case TermC.str2term "NTH 3 [a,b,c,d,e]" of
26.7 - Const ("ListC.NTH", _) $ (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _))) $
26.8 - (Const ("List.list.Cons", _) $ Free ("a", _) $
26.9 - (Const ("List.list.Cons", _) $ Free ("b", _) $
26.10 - (Const ("List.list.Cons", _) $ Free ("c", _) $
26.11 - (Const ("List.list.Cons", _) $ Free ("d", _) $
26.12 - (Const ("List.list.Cons", _) $ Free ("e", _) $ Const ("List.list.Nil", _)))))) => ()
26.13 + Const (\<^const_name>\<open>NTH\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $
26.14 + (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("a", _) $
26.15 + (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $
26.16 + (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("c", _) $
26.17 + (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("d", _) $
26.18 + (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("e", _) $ Const (\<^const_name>\<open>Nil\<close>, _)))))) => ()
26.19 | _ => error "ListC.NTH changed";
26.20 val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_CONS};
26.21 TermC.atomty thm;
26.22 @@ -105,6 +105,6 @@
26.23 val t = TermC.str2term "Length [1, 1, 1]";
26.24 val t = eval_prog_expr thy prog_expr t;
26.25 case t of
26.26 - Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _)) => ()
26.27 + Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)) => ()
26.28 | _ => error "Length [1, 1, 1] = 3 ..eval_prog_expr changed";
26.29
27.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml Mon Jul 19 15:34:54 2021 +0200
27.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Mon Jul 19 17:29:35 2021 +0200
27.3 @@ -91,7 +91,7 @@
27.4 "-------- fun eval_const -----------------------------------------------------------------------";
27.5 val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_const";
27.6 case rewrite_set_ @{theory Test} false tval_rls t of
27.7 - SOME (Const ("HOL.True", _), []) => ()
27.8 + SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
27.9 | _ => error "2 is_const CHANGED";
27.10
27.11 val t = TermC.str2term "2 * x is_const";
27.12 @@ -166,19 +166,19 @@
27.13 case eval_equ "#less_" "Orderings.ord_class.less" @{term "1 < (2::real)"} "" of
27.14 SOME
27.15 ("#less_1_2",
27.16 - Const ("HOL.Trueprop", _) $
27.17 - (Const ("HOL.eq", _) $
27.18 - (Const ("Orderings.ord_class.less", _) $ Const ("Groups.one_class.one", _) $
27.19 - (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ Const ("Num.num.One", _)))) $
27.20 - Const ("HOL.True", _))) => ()
27.21 + Const (\<^const_name>\<open>Trueprop\<close>, _) $
27.22 + (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
27.23 + (Const (\<^const_name>\<open>ord_class.less\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _) $
27.24 + (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) $
27.25 + Const (\<^const_name>\<open>True\<close>, _))) => ()
27.26 | _ => error "eval_equ 1 < 2 CHANGED";
27.27
27.28 case eval_equ "#less_" "Orderings.ord_class.less" @{term "1 < (1::real)"} "" of
27.29 SOME
27.30 ("#less_1_1",
27.31 - Const ("HOL.Trueprop", _) $
27.32 - (Const ("HOL.eq", _) $ (Const ("Orderings.ord_class.less", _) $ Const ("Groups.one_class.one", _) $ Const ("Groups.one_class.one", _)) $
27.33 - Const ("HOL.False", _))) => ()
27.34 + Const (\<^const_name>\<open>Trueprop\<close>, _) $
27.35 + (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>ord_class.less\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _)) $
27.36 + Const (\<^const_name>\<open>False\<close>, _))) => ()
27.37 | _ => error "eval_equ 1 < 1 CHANGED";
27.38
27.39
27.40 @@ -331,9 +331,9 @@
27.41 "---------fun eval_sameFunId -------------------------------------------------------------------";
27.42 val t = @{term "M_b L"}; TermC.atomty t;
27.43 val t as f1 $ _ = @{term "M_b L"};
27.44 -val t as Const ("HOL.eq", _) $ (f2 $ _) $ _ = @{term "M_b x = c + L*x"};
27.45 +val t as Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _ = @{term "M_b x = c + L*x"};
27.46 f1 = f2 (*true*);
27.47 -val (p as Const ("Prog_Expr.sameFunId",_) $
27.48 +val (p as Const (\<^const_name>\<open>sameFunId\<close>, _) $
27.49 (f1 $ _) $
27.50 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _)) =
27.51 @{term "sameFunId (M_b L) (M_b x = c + L*x)"};
27.52 @@ -355,7 +355,7 @@
27.53 "---------fun eval_filter_sameFunId ------------------------------------------------------------";
27.54 val flhs as (fid $ _) = @{term "y' L"};
27.55 val fs = @{term "[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]"};
27.56 -val (p as Const ("Prog_Expr.filter_sameFunId",_) $ (fid $ _) $ fs) =
27.57 +val (p as Const (\<^const_name>\<open>filter_sameFunId\<close>,_) $ (fid $ _) $ fs) =
27.58 @{term "filter_sameFunId (y' L) [M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]"};
27.59 val SOME (str, es) = eval_filter_sameFunId "" "Prog_Expr.filter_sameFunId" p "";
27.60 if UnparseC.term es = "(filter_sameFunId y' L [M_b x = c + L * x, y' x = c + L * x,\n y x = c + L * x]) =\n[y' x = c + L * x]" then ()
27.61 @@ -365,7 +365,7 @@
27.62 "---------fun eval_boollist2sum ----------------------------------------------------------------";
27.63 "---------fun eval_boollist2sum ----------------------------------------------------------------";
27.64 "---------fun eval_boollist2sum ----------------------------------------------------------------";
27.65 -fun lhs (Const ("HOL.eq",_) $ l $ _) = l
27.66 +fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l
27.67 | lhs t = error("lhs called with (" ^ UnparseC.term t ^ ")");
27.68 "----------- \<up> redefined due to overwritten identifier -----------";
27.69 val u_ = @{term "[]"};
27.70 @@ -378,16 +378,16 @@
27.71
27.72 val t = @{term "boollist2sum [b1 = k - 2*(q::real), b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"};
27.73 case t of
27.74 -Const ("Prog_Expr.boollist2sum", _) $
27.75 - (Const ("List.list.Cons", _) $
27.76 - (Const ("HOL.eq", _) $ Free ("b1", _) $ _ ) $
27.77 - (Const ("List.list.Cons", _) $
27.78 - (Const ("HOL.eq", _) $ Free ("b2", _) $ _ ) $
27.79 - (Const ("List.list.Cons", _) $
27.80 - (Const ("HOL.eq", _) $ Free ("b3", _) $ _ ) $
27.81 - (Const ("List.list.Cons", _) $
27.82 - (Const ("HOL.eq", _) $ Free ("b4", _) $ _ ) $
27.83 - Const ("List.list.Nil", _))))) => ()
27.84 +Const (\<^const_name>\<open>boollist2sum\<close>, _) $
27.85 + (Const (\<^const_name>\<open>Cons\<close>, _) $
27.86 + (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b1", _) $ _ ) $
27.87 + (Const (\<^const_name>\<open>Cons\<close>, _) $
27.88 + (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b2", _) $ _ ) $
27.89 + (Const (\<^const_name>\<open>Cons\<close>, _) $
27.90 + (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b3", _) $ _ ) $
27.91 + (Const (\<^const_name>\<open>Cons\<close>, _) $
27.92 + (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b4", _) $ _ ) $
27.93 + Const (\<^const_name>\<open>Nil\<close>, _))))) => ()
27.94 | _ => error "boollist2sum CHANGED";
27.95 val SOME (str, pred) = eval_boollist2sum "" "Prog_Expr.boollist2sum" t "";
27.96 if UnparseC.term pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then ()
27.97 @@ -445,7 +445,7 @@
27.98 "-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
27.99 "-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
27.100 "see: --------- search for Or_to_List ---";
27.101 -case or2list @{term True} of Const ("ListC.UniversalList", _) => ()
27.102 +case or2list @{term True} of Const (\<^const_name>\<open>UniversalList\<close>, _) => ()
27.103 | _ => error "TermC.UniversalList changed 1";
27.104 case or2list @{term False} of Const (\<^const_name>\<open>Nil\<close>, _) => ()
27.105 | _ => error "TermC.UniversalList changed 2";
28.1 --- a/test/Tools/isac/ProgLang/prog_tac.sml Mon Jul 19 15:34:54 2021 +0200
28.2 +++ b/test/Tools/isac/ProgLang/prog_tac.sml Mon Jul 19 17:29:35 2021 +0200
28.3 @@ -21,10 +21,10 @@
28.4 val {scr = Prog sc, ...} = MethodC.from_store ["Test", "sqrt-equ-test"];
28.5 case eval_leaf [] NONE TermC.empty sc of
28.6 (Expr (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
28.7 - (Const ("Test.solve_root_equ", _) $ Free ("e_e", _) $ Free ("v_v", _)) $
28.8 + (Const (\<^const_name>\<open>Test.solve_root_equ\<close>, _) $ Free ("e_e", _) $ Free ("v_v", _)) $
28.9 (Const (\<^const_name>\<open>Let\<close>, _) $
28.10 - (Const ("Tactical.Chain", _) $
28.11 - (Const ("Tactical.While", _) $ _ $
28.12 + (Const (\<^const_name>\<open>Chain\<close>, _) $
28.13 + (Const (\<^const_name>\<open>While\<close>, _) $ _ $
28.14 _ ) $
28.15 (_) $
28.16 Free ("e_e", _)) $
29.1 --- a/test/Tools/isac/ProgLang/program.sml Mon Jul 19 15:34:54 2021 +0200
29.2 +++ b/test/Tools/isac/ProgLang/program.sml Mon Jul 19 17:29:35 2021 +0200
29.3 @@ -31,7 +31,7 @@
29.4 val Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
29.5 nested $ _) =
29.6 Thm.prop_of @{thm biegelinie.simps};
29.7 -val (Const ("Biegelinie.biegelinie", _) $
29.8 +val (Const (\<^const_name>\<open>biegelinie\<close>, _) $
29.9 Var (("beam", 0), _) $
29.10 Var (("load", 0), _) $
29.11 Var (("fun_var", 0), _) $
29.12 @@ -41,7 +41,7 @@
29.13 Var (("id_der", 0), _)) = nested;
29.14 strip_comb nested;
29.15 (*val it =
29.16 - (Const ("Biegelinie.biegelinie", "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool")
29.17 + (Const (\<^const_name>\<open>biegelinie\<close>, "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool")
29.18 ,
29.19 [Var (("l", 0), "real"), Var (("q", 0), "real"), Var (("v", 0), "real"),
29.20 Var (("b", 0), "real \<Rightarrow> real"), Var (("s", 0), "bool list")]):
30.1 --- a/test/Tools/isac/Specify/i-model.sml Mon Jul 19 15:34:54 2021 +0200
30.2 +++ b/test/Tools/isac/Specify/i-model.sml Mon Jul 19 17:29:35 2021 +0200
30.3 @@ -73,19 +73,19 @@
30.4 "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L]))]"
30.5 (*+*)then () else error "INITIAL I_Model CHANGED";
30.6
30.7 -val Add (2, [1], true, "#Given", Cor ((Const ("Biegelinie.Streckenlast", _), [Free ("q_0", _)]),
30.8 +val Add (2, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]),
30.9 (Free ("q_q", _), [Free ("q_0", _)]))) = (*case*)
30.10 I_Model.check_single ctxt sel oris pbl ppc ct (*of*);
30.11 "~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) = (ctxt, sel, oris, pbl, ppc, ct);
30.12 val SOME t =(*case*) TermC.parseNEW ctxt str (*of*);
30.13 -(** )val ("", (2, [1], "#Given", Const ("Biegelinie.Streckenlast", _), [Free ("q_0", _)]), [Free ("q_0", _)]) =( **)
30.14 +(** )val ("", (2, [1], "#Given", Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), [Free ("q_0", _)]) =( **)
30.15 (**)val ("", ori', all) =(**)
30.16 (*case*) O_Model.is_known ctxt m_field o_model t (*of*);
30.17
30.18 (*+*)O_Model.single_to_string ori';
30.19 (*+*)val [Free ("q_0", _)] = all;
30.20
30.21 -(** )val ("", (2, [1], true, "#Given", Cor ((Const ("Biegelinie.Streckenlast", _), [Free ("q_0", _)]), (Free ("q_q", _), [Free ("q_0", _)])))) =( **)
30.22 +(** )val ("", (2, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), (Free ("q_q", _), [Free ("q_0", _)])))) =( **)
30.23 (**)val ("", itm) =(**)
30.24 (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);
30.25
31.1 --- a/test/Tools/isac/Specify/input-descript.sml Mon Jul 19 15:34:54 2021 +0200
31.2 +++ b/test/Tools/isac/Specify/input-descript.sml Mon Jul 19 17:29:35 2021 +0200
31.3 @@ -15,7 +15,7 @@
31.4 "-------- distinguish input to I_Model --------------------------------------------------------";
31.5 "-------- distinguish input to I_Model --------------------------------------------------------";
31.6 "----- fun Input_Descript.for_bool_list -----";
31.7 -val t as Const ("Input_Descript.relations",
31.8 +val t as Const (\<^const_name>\<open>Input_Descript.relations\<close>,
31.9 Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>bool\<close>,[])]),
31.10 Type ("Input_Descript.una", [])])) = @{term "relations"};
31.11 atomtyp (type_of t);
32.1 --- a/test/Tools/isac/Specify/m-match.sml Mon Jul 19 15:34:54 2021 +0200
32.2 +++ b/test/Tools/isac/Specify/m-match.sml Mon Jul 19 17:29:35 2021 +0200
32.3 @@ -55,7 +55,7 @@
32.4 "----------- M_Match.arguments, is_cp, O_Model.cpy_nam +with EqSystem (!) ----------------------";
32.5 "----------- M_Match.arguments, is_cp, O_Model.cpy_nam +with EqSystem (!) ----------------------";
32.6 "----------- M_Match.arguments, is_cp, O_Model.cpy_nam +with EqSystem (!) ----------------------";
32.7 -val Const ("Prog_Tac.SubProblem",_) $
32.8 +val Const (\<^const_name>\<open>SubProblem\<close>,_) $
32.9 (Const (\<^const_name>\<open>Pair\<close>,_) $
32.10 Free (dI',_) $
32.11 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =
32.12 @@ -72,15 +72,15 @@
32.13 val xxx = M_Match.arguments @{theory "EqSystem"} pats ags;
32.14 "-a2-----------------------------------------------------";
32.15 case M_Match.arguments @{theory "Isac_Knowledge"} pats ags of
32.16 - [(1, [1], "#Given", Const ("Input_Descript.equalities", _), _),
32.17 - (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
32.18 + [(1, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.equalities\<close>, _), _),
32.19 + (2, [1], "#Given", Const (\<^const_name>\<open>EqSystem.solveForVars\<close>, _),
32.20 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
32.21 - (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
32.22 + (3, [1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)])]
32.23 =>()
32.24 | _ => error "calchead.sml M_Match.arguments 2 args Nok ----------------";
32.25
32.26 "-b------------------------------------------------------";
32.27 -val Const ("Prog_Tac.SubProblem",_) $
32.28 +val Const (\<^const_name>\<open>SubProblem\<close>,_) $
32.29 (Const (\<^const_name>\<open>Pair\<close>,_) $
32.30 Free (dI',_) $
32.31 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =
32.32 @@ -96,17 +96,17 @@
32.33 val xxx = M_Match.arguments @{theory "Isac_Knowledge"} pats ags;
32.34 "-b2-----------------------------------------------------";
32.35 case M_Match.arguments @{theory "EqSystem"} pats ags of
32.36 - [(1, [1], "#Given", Const ("Input_Descript.equalities", _), _),
32.37 - (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
32.38 + [(1, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.equalities\<close>, _), _),
32.39 + (2, [1], "#Given", Const (\<^const_name>\<open>EqSystem.solveForVars\<close>, _),
32.40 [_ $ Free ("c", _) $ _,
32.41 _ $ Free ("c_2", _) $ _]),
32.42 - (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
32.43 + (3, [1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)])]
32.44 (* type of Find: [Free ("ss'''", "bool List.list")]*)
32.45 =>()
32.46 | _ => error "calchead.sml M_Match.arguments copy-named dropped --------";
32.47
32.48 "-c---ERROR case: stac is missing #Given equalities e_s--";
32.49 -val stac as Const ("Prog_Tac.SubProblem",_) $
32.50 +val stac as Const (\<^const_name>\<open>SubProblem\<close>,_) $
32.51 (Const (\<^const_name>\<open>Pair\<close>,_) $
32.52 Free (dI',_) $
32.53 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =
32.54 @@ -146,7 +146,7 @@
32.55
32.56 "-------------------------------------step through end---";
32.57 "--------- M_Match.arguments, is_cp, O_Model.cpy_nam +with EqSystem (!)--";
32.58 -val Const ("Prog_Tac.SubProblem",_) $
32.59 +val Const (\<^const_name>\<open>SubProblem\<close>,_) $
32.60 (Const (\<^const_name>\<open>Pair\<close>,_) $
32.61 Free (dI',_) $
32.62 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =
32.63 @@ -163,15 +163,15 @@
32.64 val xxx = M_Match.arguments @{theory "EqSystem"} pats ags;
32.65 "-a2-----------------------------------------------------";
32.66 case M_Match.arguments @{theory "Isac_Knowledge"} pats ags of
32.67 - [(1, [1], "#Given", Const ("Input_Descript.equalities", _), _),
32.68 - (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
32.69 + [(1, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.equalities\<close>, _), _),
32.70 + (2, [1], "#Given", Const (\<^const_name>\<open>EqSystem.solveForVars\<close>, _),
32.71 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
32.72 - (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
32.73 + (3, [1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)])]
32.74 =>()
32.75 | _ => error "calchead.sml M_Match.arguments 2 args Nok ----------------";
32.76
32.77 "-b------------------------------------------------------";
32.78 -val Const ("Prog_Tac.SubProblem",_) $
32.79 +val Const (\<^const_name>\<open>SubProblem\<close>,_) $
32.80 (Const (\<^const_name>\<open>Pair\<close>,_) $
32.81 Free (dI',_) $
32.82 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =
32.83 @@ -187,17 +187,17 @@
32.84 val xxx = M_Match.arguments @{theory "Isac_Knowledge"} pats ags;
32.85 "-b2-----------------------------------------------------";
32.86 case M_Match.arguments @{theory "EqSystem"} pats ags of
32.87 - [(1, [1], "#Given", Const ("Input_Descript.equalities", _), _),
32.88 - (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
32.89 + [(1, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.equalities\<close>, _), _),
32.90 + (2, [1], "#Given", Const (\<^const_name>\<open>EqSystem.solveForVars\<close>, _),
32.91 [_ $ Free ("c", _) $ _,
32.92 _ $ Free ("c_2", _) $ _]),
32.93 - (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
32.94 + (3, [1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)])]
32.95 (* type of Find: [Free ("ss'''", "bool List.list")]*)
32.96 =>()
32.97 | _ => error "calchead.sml M_Match.arguments copy-named dropped --------";
32.98
32.99 "-c---ERROR case: stac is missing #Given equalities e_s--";
32.100 -val stac as Const ("Prog_Tac.SubProblem",_) $
32.101 +val stac as Const (\<^const_name>\<open>SubProblem\<close>,_) $
32.102 (Const (\<^const_name>\<open>Pair\<close>,_) $
32.103 Free (dI',_) $
32.104 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =
32.105 @@ -242,7 +242,7 @@
32.106 | _ => error "calchead.sml M_Match.arguments 1st arg missing --------";
32.107
32.108 "-d------------------------------------------------------";
32.109 -val stac as Const ("Prog_Tac.SubProblem",_) $
32.110 +val stac as Const (\<^const_name>\<open>SubProblem\<close>,_) $
32.111 (Const (\<^const_name>\<open>Pair\<close>,_) $
32.112 Free (dI',_) $
32.113 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =
32.114 @@ -260,7 +260,7 @@
32.115 | _ => error "calchead.sml M_Match.arguments 1st arg missing --------";
32.116
32.117 "-d------------------------------------------------------";
32.118 -val stac as Const ("Prog_Tac.SubProblem",_) $
32.119 +val stac as Const (\<^const_name>\<open>SubProblem\<close>, _) $
32.120 (Const (\<^const_name>\<open>Pair\<close>,_) $
32.121 Free (dI',_) $
32.122 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =
32.123 @@ -341,10 +341,10 @@
32.124 "-------------------------------------step through end---";
32.125
32.126 case M_Match.arguments thy PATS AGS of
32.127 -[(1, [1], "#Given", Const ("Input_Descript.equality", _),
32.128 - [Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $
32.129 +[(1, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.equality\<close>, _),
32.130 + [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>plus_class.plus\<close>, _) $
32.131 Free ("x", _) $ _(*1*)) $ _(*1*)]),
32.132 - (2, [1], "#Given", Const ("Input_Descript.solveFor", _), [Free ("x", _)]),
32.133 - (3, [1], "#Find", Const ("Input_Descript.solutions", _), [Free ("x_i", _)])]
32.134 + (2, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.solveFor\<close>, _), [Free ("x", _)]),
32.135 + (3, [1], "#Find", Const (\<^const_name>\<open>Input_Descript.solutions\<close>, _), [Free ("x_i", _)])]
32.136 => ()
32.137 | _ => error "calchead.sml M_Match.arguments [univariate,equation,test]--";
33.1 --- a/test/Tools/isac/Specify/o-model.sml Mon Jul 19 15:34:54 2021 +0200
33.2 +++ b/test/Tools/isac/Specify/o-model.sml Mon Jul 19 17:29:35 2021 +0200
33.3 @@ -50,29 +50,29 @@
33.4 |> add_variants;
33.5
33.6 (*+ decompose..*)
33.7 -(*+*)val aaa as Const ("Biegelinie.Traegerlaenge", _) $ Free ("L", _) = (nth 1 fmz) |> TermC.parseNEW'' thy;
33.8 -(*+*)val bbb as (Const ("Biegelinie.Traegerlaenge", _), [Free ("L", _)]) = aaa |> Input_Descript.split;
33.9 -(*+*)val ccc as ("#Given", Const ("Biegelinie.Traegerlaenge", _), [Free ("L", _)]) = bbb |> add_field thy pbt;
33.10 +(*+*)val aaa as Const (\<^const_name>\<open>Traegerlaenge\<close>, _) $ Free ("L", _) = (nth 1 fmz) |> TermC.parseNEW'' thy;
33.11 +(*+*)val bbb as (Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]) = aaa |> Input_Descript.split;
33.12 +(*+*)val ccc as ("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]) = bbb |> add_field thy pbt;
33.13 (*+ WHY IS THE LIST IN "#Relate" NOT DECOMPOSED?...*)
33.14 -(*+*)val ddd as [("#Given", Const ("Biegelinie.Traegerlaenge", _), [Free ("L", _)]),
33.15 - ("#Given", Const ("Biegelinie.Streckenlast", _), [Free ("q_0", _)]),
33.16 - ("#Find", Const ("Biegelinie.Biegelinie", _), [Free ("y", _)]),
33.17 - ("#Relate", Const ("Biegelinie.Randbedingungen", _),
33.18 - [Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ (Free ("y", _) $ _(*"0"*)) $ _(*"0"*)) $
33.19 - Const ("List.list.Nil", _),
33.20 - Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ (Free ("y", _) $ _(**)) $ _(*"0"*)) $
33.21 - Const ("List.list.Nil", _),
33.22 - Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ (Const ("Biegelinie.M_b", _) $ _(*"0"*)) $ _(*"0"*)) $
33.23 - Const ("List.list.Nil", _),
33.24 - Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ (Const ("Biegelinie.M_b", _) $ Free ("L", _)) $ _(*"0"*)) $
33.25 - Const ("List.list.Nil", _)]),
33.26 - ("#undef", Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]),
33.27 +(*+*)val ddd as [("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]),
33.28 + ("#Given", Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]),
33.29 + ("#Find", Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]),
33.30 + ("#Relate", Const (\<^const_name>\<open>Randbedingungen\<close>, _),
33.31 + [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Free ("y", _) $ _(*"0"*)) $ _(*"0"*)) $
33.32 + Const (\<^const_name>\<open>Nil\<close>, _),
33.33 + Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Free ("y", _) $ _(**)) $ _(*"0"*)) $
33.34 + Const (\<^const_name>\<open>Nil\<close>, _),
33.35 + Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>Biegelinie.M_b\<close>, _) $ _(*"0"*)) $ _(*"0"*)) $
33.36 + Const (\<^const_name>\<open>Nil\<close>, _),
33.37 + Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>Biegelinie.M_b\<close>, _) $ Free ("L", _)) $ _(*"0"*)) $
33.38 + Const (\<^const_name>\<open>Nil\<close>, _)]),
33.39 + ("#undef", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]),
33.40 _, _] =
33.41 (map (fn str => str
33.42 |> TermC.parseNEW'' thy
33.43 |> Input_Descript.split
33.44 |> add_field thy pbt) fmz);
33.45 -(*+*)val eee as [(0, ("#Given", Const ("Biegelinie.Traegerlaenge", _), [Free ("L", _)])),
33.46 +(*+*)val eee as [(0, ("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)])),
33.47 _, _, _, _, _, _] = add_variants ddd;
33.48
33.49 val maxv = map fst ori |> max;
33.50 @@ -160,17 +160,17 @@
33.51
33.52 case o_model of
33.53 [
33.54 - (1, [1, 2, 3], "#Given", Const ("Input_Descript.fixedValues", _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const ("Program.Arbfix", _)) $ _]),
33.55 - (2, [1, 2, 3], "#Find", Const ("Input_Descript.maximum", _), [Free ("A", _)]),
33.56 - (3, [1, 2, 3], "#Find", Const ("Input_Descript.valuesFor", _), [_ $ Free ("a", _) $ _, Const ("List.list.Cons", _) $ Free ("b", _) $ _]),
33.57 - (4, [1, 2], "#Relate", Const ("Input_Descript.relations", _), _),
33.58 - (5, [3], "#Relate", Const ("Input_Descript.relations", _), _),
33.59 - (6, [1], "#undef", Const ("Input_Descript.boundVariable", _), [Free ("a", _)]),
33.60 - (7, [2], "#undef", Const ("Input_Descript.boundVariable", _), [Free ("b", _)]),
33.61 - (8, [3], "#undef", Const ("Input_Descript.boundVariable", _), [Free ("alpha", _)]),
33.62 - (9, [1, 2], "#undef", Const ("Input_Descript.interval", _), [Const (\<^const_name>\<open>Collect\<close>, _) $ Abs ("x", _, Const (\<^const_name>\<open>conj\<close>, _) $ _ $ _)]),
33.63 - (10, [3], "#undef", Const ("Input_Descript.interval", _), _),
33.64 - (11, [1, 2, 3], "#undef", Const ("Input_Descript.errorBound", _), [Const ("HOL.eq", _) $ Free ("eps", _) $ _(*"0"*)])
33.65 + (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]),
33.66 + (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
33.67 + (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
33.68 + (4, [1, 2], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
33.69 + (5, [3], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
33.70 + (6, [1], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("a", _)]),
33.71 + (7, [2], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("b", _)]),
33.72 + (8, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("alpha", _)]),
33.73 + (9, [1, 2], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), [Const (\<^const_name>\<open>Collect\<close>, _) $ Abs ("x", _, Const (\<^const_name>\<open>conj\<close>, _) $ _ $ _)]),
33.74 + (10, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), _),
33.75 + (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
33.76 ] => ()
33.77 | _ => error "fun O_Model.init CHANGED";
33.78
33.79 @@ -184,29 +184,29 @@
33.80
33.81 case filtered of
33.82 [[
33.83 - (1, [1, 2, 3], "#Given", Const ("Input_Descript.fixedValues", _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const ("Program.Arbfix", _)) $ _]),
33.84 - (2, [1, 2, 3], "#Find", Const ("Input_Descript.maximum", _), [Free ("A", _)]),
33.85 - (3, [1, 2, 3], "#Find", Const ("Input_Descript.valuesFor", _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
33.86 - (4, [1, 2], "#Relate", Const ("Input_Descript.relations", _), _),
33.87 - (6, [1], "#undef", Const ("Input_Descript.boundVariable", _), [Free ("a", _)]),
33.88 - (9, [1, 2], "#undef", Const ("Input_Descript.interval", _), [Const ("Set.Collect", _) $ Abs ("x", _, Const ("HOL.conj", _) $ _ $ _)]),
33.89 - (11, [1, 2, 3], "#undef", Const ("Input_Descript.errorBound", _), [Const ("HOL.eq", _) $ Free ("eps", _) $ _(*"0"*)])
33.90 + (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]),
33.91 + (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
33.92 + (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
33.93 + (4, [1, 2], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
33.94 + (6, [1], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("a", _)]),
33.95 + (9, [1, 2], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), [Const (\<^const_name>\<open>Collect\<close>, _) $ Abs ("x", _, Const (\<^const_name>\<open>conj\<close>, _) $ _ $ _)]),
33.96 + (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
33.97 ], [
33.98 - (1, [1, 2, 3], "#Given", Const ("Input_Descript.fixedValues", _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const ("Program.Arbfix", _)) $ _]),
33.99 - (2, [1, 2, 3], "#Find", Const ("Input_Descript.maximum", _), [Free ("A", _)]),
33.100 - (3, [1, 2, 3], "#Find", Const ("Input_Descript.valuesFor", _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
33.101 - (4, [1, 2], "#Relate", Const ("Input_Descript.relations", _), _),
33.102 - (7, [2], "#undef", Const ("Input_Descript.boundVariable", _), [Free ("b", _)]),
33.103 - (9, [1, 2], "#undef", Const ("Input_Descript.interval", _), [Const ("Set.Collect", _) $ Abs ("x", _, Const ("HOL.conj", _) $ _ $ _)]),
33.104 - (11, [1, 2, 3], "#undef", Const ("Input_Descript.errorBound", _), [Const ("HOL.eq", _) $ Free ("eps", _) $ _(*"0"*)])
33.105 + (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]),
33.106 + (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
33.107 + (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
33.108 + (4, [1, 2], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
33.109 + (7, [2], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("b", _)]),
33.110 + (9, [1, 2], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), [Const (\<^const_name>\<open>Collect\<close>, _) $ Abs ("x", _, Const (\<^const_name>\<open>conj\<close>, _) $ _ $ _)]),
33.111 + (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
33.112 ], [
33.113 - (1, [1, 2, 3], "#Given", Const ("Input_Descript.fixedValues", _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const ("Program.Arbfix", _)) $ _]),
33.114 - (2, [1, 2, 3], "#Find", Const ("Input_Descript.maximum", _), [Free ("A", _)]),
33.115 - (3, [1, 2, 3], "#Find", Const ("Input_Descript.valuesFor", _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
33.116 - (5, [3], "#Relate", Const ("Input_Descript.relations", _), _),
33.117 - (8, [3], "#undef", Const ("Input_Descript.boundVariable", _), [Free ("alpha", _)]),
33.118 - (10, [3], "#undef", Const ("Input_Descript.interval", _), _),
33.119 - (11, [1, 2, 3], "#undef", Const ("Input_Descript.errorBound", _), [Const ("HOL.eq", _) $ Free ("eps", _) $ _(*"0"*)])
33.120 + (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]),
33.121 + (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
33.122 + (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
33.123 + (5, [3], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
33.124 + (8, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("alpha", _)]),
33.125 + (10, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), _),
33.126 + (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
33.127 ]] => ()
33.128 | _ => error "fun O_Model.filter_vat CHANGED";
33.129
33.130 @@ -242,7 +242,7 @@
33.131 (*...all must be true*)
33.132
33.133 case O_Model.cpy_nam pbt oris (hd cy) of
33.134 - ([1], "#Find", Const ("Input_Descript.solutions", _), [Free ("x_i", _)]) => ()
33.135 + ([1], "#Find", Const (\<^const_name>\<open>Input_Descript.solutions\<close>, _), [Free ("x_i", _)]) => ()
33.136 | _ => error "calchead.sml regr.test O_Model.cpy_nam-1-";
33.137
33.138 (*new data: O_Model.cpy_nam without changing the name*)
33.139 @@ -259,6 +259,6 @@
33.140 (*could be more than 1*)];
33.141
33.142 case O_Model.cpy_nam pbt oris (hd cy) of
33.143 - ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => ()
33.144 + ([1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)]) => ()
33.145 | _ => error "calchead.sml regr.test O_Model.cpy_nam-2-";
33.146
34.1 --- a/test/Tools/isac/Specify/specify.sml Mon Jul 19 15:34:54 2021 +0200
34.2 +++ b/test/Tools/isac/Specify/specify.sml Mon Jul 19 17:29:35 2021 +0200
34.3 @@ -463,7 +463,7 @@
34.4 (*if*) icl = [] (*else*);
34.5 val SOME ori =(*case*) find_first (test_subset (hd icl)) vors (*of*);
34.6
34.7 -(*+*)val (5, [1], "#Given", Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]) = ori
34.8 +(*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) = ori
34.9 (*+*)val SOME ("#Given", "FunktionsVariable x") =
34.10
34.11 SOME
34.12 @@ -497,7 +497,7 @@
34.13 val (i_model, m_patt) = (met,
34.14 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store |> #ppc)
34.15
34.16 -val Add (5, [1], true, "#Given", Cor ((Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), (Free ("fun_var", _), [Free ("x", _)]))) =
34.17 +val Add (5, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), (Free ("fun_var", _), [Free ("x", _)]))) =
34.18 (*case*)
34.19 I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
34.20 "~~~~~ ~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
34.21 @@ -505,7 +505,7 @@
34.22 (*.NEW*) val SOME (t as (descriptor $ _)) = (*case*) TermC.parseNEW ctxt str (*of*);
34.23 (*.NEW*) val SOME m_field = (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
34.24
34.25 -val ("", (5, [1], "#Given", Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), [Free ("x", _)]) =
34.26 +val ("", (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), [Free ("x", _)]) =
34.27 (*case*)
34.28 O_Model.is_known ctxt m_field o_model t (*of*);
34.29 "~~~~~ ~~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
34.30 @@ -524,7 +524,7 @@
34.31 (*/------------------- check within seek_oridts --------------------------------------------\*)
34.32 (*+*)val Add_Given "FunktionsVariable x" = tac;
34.33 (*+*)m_field = "#Given";
34.34 -(*+*)val Const ("Biegelinie.FunktionsVariable", _) = descript;
34.35 +(*+*)val Const (\<^const_name>\<open>FunktionsVariable\<close>, _) = descript;
34.36 (*+*)val [Free ("x", _)] = vals;
34.37 (*+*)O_Model.to_string ori = "[\n" ^
34.38 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
34.39 @@ -535,7 +535,7 @@
34.40 "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
34.41 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]";
34.42 (*+*)val (id, vat, m_field', descript', vals') = nth 5 ori
34.43 -(*+*)val (5, [1], "#Given", Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]) =
34.44 +(*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) =
34.45 (id, vat, m_field', descript', vals')
34.46 (*\------------------- check within seek_oridts --------------------------------------------/*)
34.47 (*-------------------- stop step into whole me ----------------------------------------------*)
34.48 @@ -780,7 +780,7 @@
34.49 val (i_model, m_patt) = (met,
34.50 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store |> #ppc)
34.51
34.52 -val Add (4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", _), [Free ("y", _)]), (Free ("id_fun", _), [Free ("y", _)]))) =
34.53 +val Add (4, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]), (Free ("id_fun", _), [Free ("y", _)]))) =
34.54 (*case*)
34.55 check_single ctxt m_field oris i_model m_patt ct (*of*);
34.56
34.57 @@ -805,9 +805,9 @@
34.58 (ctxt, sel, oris, met, ((#ppc o MethodC.from_store) cmI), ct);
34.59 val SOME t = (*case*) TermC.parseNEW ctxt str (*of*);
34.60
34.61 -(*+*)val Const ("Biegelinie.Biegelinie", _) $ Free ("y", _) = t;
34.62 +(*+*)val Const (\<^const_name>\<open>Biegelinie\<close>, _) $ Free ("y", _) = t;
34.63
34.64 -(*("seek_oridts: input ('Biegelinie y') not found in oris (typed)", (0, [], "#Given", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]), [])*)
34.65 +(*("seek_oridts: input ('Biegelinie y') not found in oris (typed)", (0, [], "#Given", Const (\<^const_name>\<open>Biegelinie\<close>, "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]), [])*)
34.66 (*case*)
34.67 is_known ctxt m_field o_model t (*of*);
34.68 "~~~~~ ~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
35.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Jul 19 15:34:54 2021 +0200
35.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Jul 19 17:29:35 2021 +0200
35.3 @@ -167,7 +167,7 @@
35.4 -------------------------------------------------------------------------ARE AT THE RIGHT MARGIN*)
35.5 section \<open>trials with Isabelle's functions\<close>
35.6 ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
35.7 - ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
35.8 + ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
35.9 ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML"
35.10 ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML"
35.11 ML_file "$ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML"
35.12 @@ -329,7 +329,9 @@
35.13 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
35.14 ML \<open>
35.15 \<close> ML \<open>
35.16 +@{term Let}
35.17 \<close> ML \<open>
35.18 +val Const (\<^const_name>\<open>Let\<close>, _) = @{term Let}
35.19 \<close> ML \<open>
35.20 \<close> ML \<open>
35.21 \<close> ML \<open>
36.1 --- a/test/Tools/isac/Test_Some.thy Mon Jul 19 15:34:54 2021 +0200
36.2 +++ b/test/Tools/isac/Test_Some.thy Mon Jul 19 17:29:35 2021 +0200
36.3 @@ -1213,12 +1213,12 @@
36.4 (*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*)
36.5 val t = (Thm.term_of o the o (TermC.parse thy)) "Not (x =!= a)";
36.6 case rewrite_set_ thy false erls_diff t of
36.7 - SOME (Const ("HOL.True", _), []) => ()
36.8 + SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
36.9 | _ => error "rewrite_set_ Not (x =!= a) changed";
36.10
36.11 val t =(Thm.term_of o the o (TermC.parse thy)) "2 is_const";
36.12 case rewrite_set_ thy false erls_diff t of
36.13 - SOME (Const ("HOL.True", _), []) => ()
36.14 + SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
36.15 | _ => error "rewrite_set_ 2 is_const changed";
36.16
36.17 val thm = @{thm diff_const};
36.18 @@ -1649,12 +1649,12 @@
36.19 val t = TermC.str2term "Integral x D x";
36.20 val t = TermC.str2term "Integral x \<up> 2 D x";
36.21 case t of
36.22 - Const ("Integrate.Integral", _) $
36.23 - (Const ("Transcendental.powr", _) $ Free _ $ _) $ Free ("x", _) => ()
36.24 + Const (\<^const_name>\<open>Integral\<close>, _) $
36.25 + (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ _) $ Free ("x", _) => ()
36.26 | _ => error "integrate.sml: parsing: Integral x \<up> 2 D x";
36.27
36.28 val t = TermC.str2term "ff x is_f_x";
36.29 -case t of Const ("Integrate.is_f_x", _) $ _ => ()
36.30 +case t of Const (\<^const_name>\<open>is_f_x\<close>, _) $ _ => ()
36.31 | _ => error "integrate.sml: parsing: ff x is_f_x";
36.32
36.33
36.34 @@ -1967,7 +1967,7 @@
36.35 val t1 = (Thm.term_of o hd) chkmodel;
36.36 val t2 = (Thm.term_of o hd o tl) chkmodel;
36.37 val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
36.38 -case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()
36.39 +case t3 of Const (\<^const_name>\<open>antiDerivative\<close>, _) $ _ => ()
36.40 | _ => error "integrate.sml: Integrate.antiDerivative ???";
36.41
36.42 \<close> ML \<open>
36.43 @@ -1980,19 +1980,19 @@
36.44 val t1 = (Thm.term_of o hd) chkmodel;
36.45 val t2 = (Thm.term_of o hd o tl) chkmodel;
36.46 val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
36.47 -case t3 of Const ("Integrate.antiDerivativeName", _) $ _ => ()
36.48 +case t3 of Const (\<^const_name>\<open>antiDerivativeName\<close>, _) $ _ => ()
36.49 | _ => error "integrate.sml: Integrate.antiDerivativeName";
36.50
36.51 \<close> ML \<open>
36.52 "----- compare 'Find's from problem, script, formalization -------";
36.53 val {ppc,...} = Problem.from_store ["named", "integrate", "function"];
36.54 -val ("#Find", (Const ("Integrate.antiDerivativeName", _),
36.55 +val ("#Find", (Const (\<^const_name>\<open>antiDerivativeName\<close>, _),
36.56 F1_ as Free ("F_F", F1_type))) = last_elem ppc;
36.57 val {scr = Prog sc,... } = MethodC.from_store ["diff", "integration", "named"];
36.58 val [_,_, F2_] = formal_args sc;
36.59 if F1_ = F2_ then () else error "integrate.sml: unequal find's";
36.60
36.61 -val ((dsc as Const ("Integrate.antiDerivativeName", _))
36.62 +val ((dsc as Const (\<^const_name>\<open>antiDerivativeName\<close>, _))
36.63 $ Free ("ff", F3_type)) = TermC.str2term "antiDerivativeName ff";
36.64 if Input_Descript.is_a dsc then () else error "integrate.sml: no description";
36.65 if F1_type = F3_type then ()
36.66 @@ -2000,7 +2000,7 @@
36.67
36.68 Test_Tool.show_ptyps();
36.69 val pbl = Problem.from_store ["integrate", "function"];
36.70 -case #cas pbl of SOME (Const ("Integrate.Integrate",_) $ _) => ()
36.71 +case #cas pbl of SOME (Const (\<^const_name>\<open>Integrate\<close>, _) $ _) => ()
36.72 | _ => error "integrate.sml: Integrate.Integrate ???";
36.73
36.74