src/Tools/isac/Knowledge/Inverse_Z_Transform.thy
changeset 42451 bc03b5d60547
parent 42425 da7fbace995b
child 52125 6f1d3415dc68
     1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Jul 30 16:41:08 2012 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Tue Jul 31 15:16:47 2012 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  ML {*
     1.5  val inverse_z = prep_rls(
     1.6    Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",dummy_ord), 
     1.7 -	  erls = Erls, srls = Erls, calc = [],
     1.8 +	  erls = Erls, srls = Erls, calc = [], errpatts = [],
     1.9  	  rules = 
    1.10  	   [
    1.11      Thm ("rule4",num_str @{thm rule4})
    1.12 @@ -222,7 +222,7 @@
    1.13          Calc ("Orderings.ord_class.less",eval_equ "#less_"),
    1.14          (*2nd NTH_CONS pushes n+-1 into asms*)
    1.15          Calc("Groups.plus_class.plus", eval_binop "#add_")], 
    1.16 -        srls = Erls, calc = [],
    1.17 +        srls = Erls, calc = [], errpatts = [],
    1.18          rules = [
    1.19            Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
    1.20            Calc("Groups.plus_class.plus", eval_binop "#add_"),