equal
deleted
inserted
replaced
381 .. |
381 .. |
382 |
382 |
383 |
383 |
384 subsubsection "Tests" |
384 subsubsection "Tests" |
385 |
385 |
386 (* FIXME dirty trick to get around some problem with the code generator *) |
386 (* Trick to make the code generator happy. *) |
387 lemma [code]: "equal_class.equal (x::'a st) y = equal_class.equal x y" |
387 lemma [code]: "equal_class.equal (x::'a st) y = equal_class.equal x y" |
388 by(rule refl) |
388 by(rule refl) |
389 |
389 |
390 definition "step_up_ivl n = |
390 definition "step_up_ivl n = |
391 ((\<lambda>C. C \<nabla> step_ivl (top(strip C)) C)^^n)" |
391 ((\<lambda>C. C \<nabla> step_ivl (top(strip C)) C)^^n)" |