equal
deleted
inserted
replaced
25 filterExpression :: "bool => una" |
25 filterExpression :: "bool => una" |
26 stepResponse :: "bool => una" |
26 stepResponse :: "bool => una" |
27 |
27 |
28 |
28 |
29 ML {* |
29 ML {* |
30 val inverse_z = prep_rls( |
30 val inverse_z = prep_rls'( |
31 Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",dummy_ord), |
31 Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",dummy_ord), |
32 erls = Erls, srls = Erls, calc = [], errpatts = [], |
32 erls = Erls, srls = Erls, calc = [], errpatts = [], |
33 rules = |
33 rules = |
34 [ |
34 [ |
35 Thm ("rule4",num_str @{thm rule4}) |
35 Thm ("rule4",num_str @{thm rule4}) |