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_"),