1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Jun 21 14:39:52 2021 +0200
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Jun 21 15:36:09 2021 +0200
1.3 @@ -183,7 +183,7 @@
1.4 ML \<open>
1.5 val (_, expr) = HOLogic.dest_eq fun3'; UnparseC.term expr;
1.6 val (_, denom) =
1.7 - HOLogic.dest_bin "Rings.divide_class.divide" (type_of expr) expr;
1.8 + HOLogic.dest_bin \<^const_name>\<open>divide\<close> (type_of expr) expr;
1.9 UnparseC.term denom = "-1 + -2 * z + 8 * z \<up> 2";
1.10 \<close>
1.11
1.12 @@ -217,7 +217,7 @@
1.13 *)
1.14 fun eval_get_denominator (thmid:string) _
1.15 (t as Const ("Rational.get_denominator", _) $
1.16 - (Const ("Rings.divide_class.divide", _) $num
1.17 + (Const (\<^const_name>\<open>divide\<close>, _) $num
1.18 $denom)) thy =
1.19 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy denom) "",
1.20 HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
1.21 @@ -237,7 +237,7 @@
1.22 *)
1.23 fun eval_get_numerator (thmid:string) _
1.24 (t as Const ("Rational.get_numerator", _) $
1.25 - (Const ("Rings.divide_class.divide", _) $num
1.26 + (Const (\<^const_name>\<open>divide\<close>, _) $num
1.27 $denom )) thy =
1.28 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy num) "",
1.29 HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
1.30 @@ -348,8 +348,8 @@
1.31 \<close>
1.32
1.33 ML \<open>
1.34 - val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _)
1.35 - $ s_2 $ Const ("List.list.Nil", _)) = solutions;
1.36 + val Const (\<^const_name>\<open>Cons\<close>, _) $ s_1 $ (Const (\<^const_name>\<open>Cons\<close>, _)
1.37 + $ s_2 $ Const (\<^const_name>\<open>Nil\<close>, _)) = solutions;
1.38 UnparseC.term s_1;
1.39 UnparseC.term s_2;
1.40 \<close>
1.41 @@ -366,9 +366,9 @@
1.42
1.43 ML \<open>
1.44 val xx = HOLogic.dest_eq s_1;
1.45 - val s_1' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
1.46 + val s_1' = HOLogic.mk_binop \<^const_name>\<open>minus\<close> xx;
1.47 val xx = HOLogic.dest_eq s_2;
1.48 - val s_2' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
1.49 + val s_2' = HOLogic.mk_binop \<^const_name>\<open>minus\<close> xx;
1.50 UnparseC.term s_1';
1.51 UnparseC.term s_2';
1.52 \<close>
1.53 @@ -379,7 +379,7 @@
1.54 ML \<open>
1.55 fun fac_from_sol s =
1.56 let val (lhs, rhs) = HOLogic.dest_eq s
1.57 - in HOLogic.mk_binop "Groups.minus_class.minus" (lhs, rhs) end;
1.58 + in HOLogic.mk_binop \<^const_name>\<open>minus\<close> (lhs, rhs) end;
1.59 \<close>
1.60
1.61 ML \<open>
1.62 @@ -390,16 +390,16 @@
1.63 | mk_prod prod (t :: []) =
1.64 if prod = TermC.empty
1.65 then t
1.66 - else HOLogic.mk_binop "Groups.times_class.times" (prod, t)
1.67 + else HOLogic.mk_binop \<^const_name>\<open>times\<close> (prod, t)
1.68 | mk_prod prod (t1 :: t2 :: ts) =
1.69 if prod = TermC.empty
1.70 then
1.71 let val p =
1.72 - HOLogic.mk_binop "Groups.times_class.times" (t1, t2)
1.73 + HOLogic.mk_binop \<^const_name>\<open>times\<close> (t1, t2)
1.74 in mk_prod p ts end
1.75 else
1.76 let val p =
1.77 - HOLogic.mk_binop "Groups.times_class.times" (prod, t1)
1.78 + HOLogic.mk_binop \<^const_name>\<open>times\<close> (prod, t1)
1.79 in mk_prod p (t2 :: ts) end
1.80 \<close>
1.81 (* ML {*
1.82 @@ -585,11 +585,11 @@
1.83 *)
1.84
1.85 val denominator' = HOLogic.mk_binop
1.86 - "Groups.times_class.times" (s_1', s_2') ;
1.87 + \<^const_name>\<open>times\<close> (s_1', s_2') ;
1.88 val SOME numerator = parseNEW ctxt "3::real";
1.89
1.90 val expr' = HOLogic.mk_binop
1.91 - "Rings.divide_class.divide" (numerator, denominator');
1.92 + \<^const_name>\<open>divide\<close> (numerator, denominator');
1.93 UnparseC.term expr';
1.94 \<close>
1.95
1.96 @@ -1092,14 +1092,14 @@
1.97 rew_ord = ("termlessI",termlessI),
1.98 erls = Rule_Set.append_rules "erls_in_srls_InverseZTransform" Rule_Set.empty
1.99 [(*for asm in NTH_CONS ...*)
1.100 - Eval ("Orderings.ord_class.less",eval_equ "#less_"),
1.101 + Eval (\<^const_name>\<open>less\<close>,eval_equ "#less_"),
1.102 (*2nd NTH_CONS pushes n+-1 into asms*)
1.103 - Eval("Groups.plus_class.plus", eval_binop "#add_")
1.104 + Eval(\<^const_name>\<open>plus\<close>, eval_binop "#add_")
1.105 ],
1.106 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.107 rules = [
1.108 Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.109 - Eval("Groups.plus_class.plus", eval_binop "#add_"),
1.110 + Eval(\<^const_name>\<open>plus\<close>, eval_binop "#add_"),
1.111 Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
1.112 Eval("Prog_Expr.lhs", eval_lhs"eval_lhs_"),
1.113 Eval("Prog_Expr.rhs", eval_rhs"eval_rhs_"),
1.114 @@ -1220,7 +1220,7 @@
1.115 [1],
1.116 "#Given",
1.117 Const ("Inverse_Z_Transform.filterExpression", _),
1.118 - [Const ("HOL.eq", _) $ _ $ _]
1.119 + [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _]
1.120 ),
1.121 (
1.122 2,