| changeset 42814 | 5af15f1e2ef6 |
| parent 42284 | 326f57825e1a |
| child 44241 | 7943b69f0188 |
--- a/src/CCL/Term.thy Sun May 15 17:06:35 2011 +0200 +++ b/src/CCL/Term.thy Sun May 15 17:45:53 2011 +0200 @@ -205,7 +205,7 @@ Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED o simp_tac (simpset_of ctxt addsimps @{thms rawBs} setloop (stac @{thm letrecB})))) -*} "" +*} lemma ifBtrue: "if true then t else u = t" and ifBfalse: "if false then t else u = u"