equal
deleted
inserted
replaced
201 lemmas rawBs = caseBs applyB applyBbot |
201 lemmas rawBs = caseBs applyB applyBbot |
202 |
202 |
203 method_setup beta_rl = {* |
203 method_setup beta_rl = {* |
204 Scan.succeed (fn ctxt => |
204 Scan.succeed (fn ctxt => |
205 SIMPLE_METHOD' (CHANGED o |
205 SIMPLE_METHOD' (CHANGED o |
206 simp_tac (ctxt addsimps @{thms rawBs} setloop (fn _ => stac @{thm letrecB})))) |
206 simp_tac (ctxt addsimps @{thms rawBs} setloop (fn _ => stac ctxt @{thm letrecB})))) |
207 *} |
207 *} |
208 |
208 |
209 lemma ifBtrue: "if true then t else u = t" |
209 lemma ifBtrue: "if true then t else u = t" |
210 and ifBfalse: "if false then t else u = u" |
210 and ifBfalse: "if false then t else u = u" |
211 and ifBbot: "if bot then t else u = bot" |
211 and ifBbot: "if bot then t else u = bot" |