1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Sat Jun 12 18:06:27 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Sat Jun 12 18:22:07 2021 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  	  erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
     1.5  	  rules = 
     1.6  	   [
     1.7 -    Rule.Thm ("rule4", @{thm rule4})
     1.8 +    \<^rule_thm>\<open>rule4\<close>
     1.9  	   ], 
    1.10  	 scr = Rule.Empty_Prog});
    1.11  \<close>
    1.12 @@ -126,9 +126,9 @@
    1.13                      (*2nd NTH_CONS pushes n+-1 into asms*)
    1.14                      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], 
    1.15                srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.16 -              rules = [Rule.Thm ("NTH_CONS", @{thm NTH_CONS}),
    1.17 +              rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
    1.18                    \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
    1.19 -                  Rule.Thm ("NTH_NIL", @{thm NTH_NIL}),
    1.20 +                  \<^rule_thm>\<open>NTH_NIL\<close>,
    1.21                    \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
    1.22                    \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
    1.23                    \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),