changeset 51717 | 9e7d1c139569 |
parent 51670 | d721d21e6374 |
child 52037 | 837211662fb8 |
--- a/src/CCL/Term.thy Tue Apr 16 17:54:14 2013 +0200 +++ b/src/CCL/Term.thy Thu Apr 18 17:07:01 2013 +0200 @@ -204,7 +204,7 @@ method_setup beta_rl = {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED o - simp_tac (simpset_of ctxt addsimps @{thms rawBs} setloop (stac @{thm letrecB})))) + simp_tac (ctxt addsimps @{thms rawBs} setloop (stac @{thm letrecB})))) *} lemma ifBtrue: "if true then t else u = t"