equal
deleted
inserted
replaced
25 filterExpression :: "bool => una" |
25 filterExpression :: "bool => una" |
26 stepResponse :: "bool => una" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6 above\<close> |
26 stepResponse :: "bool => una" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6 above\<close> |
27 |
27 |
28 ML \<open> |
28 ML \<open> |
29 val inverse_z = prep_rls'( |
29 val inverse_z = prep_rls'( |
30 Rule_Def.Repeat {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
30 Rule_Def.Repeat {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), |
31 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
31 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
32 rules = |
32 rules = |
33 [ |
33 [ |
34 \<^rule_thm>\<open>rule4\<close> |
34 \<^rule_thm>\<open>rule4\<close> |
35 ], |
35 ], |