1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Sun Feb 25 16:31:17 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Fri Mar 02 14:19:59 2018 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  	  erls = Erls, srls = Erls, calc = [], errpatts = [],
     1.5  	  rules = 
     1.6  	   [
     1.7 -    Thm ("rule4",num_str @{thm rule4})
     1.8 +    Thm ("rule4", @{thm rule4})
     1.9  	   ], 
    1.10  	 scr = EmptyScr}:rls);
    1.11  *}
    1.12 @@ -188,9 +188,9 @@
    1.13                      (*2nd NTH_CONS pushes n+-1 into asms*)
    1.14                      Calc("Groups.plus_class.plus", eval_binop "#add_")], 
    1.15                srls = Erls, calc = [], errpatts = [],
    1.16 -              rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
    1.17 +              rules = [Thm ("NTH_CONS", @{thm NTH_CONS}),
    1.18                    Calc ("Groups.plus_class.plus", eval_binop "#add_"),
    1.19 -                  Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
    1.20 +                  Thm ("NTH_NIL", @{thm NTH_NIL}),
    1.21                    Calc ("Tools.lhs", eval_lhs "eval_lhs_"),
    1.22                    Calc ("Tools.rhs", eval_rhs"eval_rhs_"),
    1.23                    Calc ("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),