--- a/src/HOLCF/Lift.thy Fri Mar 20 11:26:59 2009 +0100
+++ b/src/HOLCF/Lift.thy Fri Mar 20 15:24:18 2009 +0100
@@ -56,15 +56,13 @@
by (cases x) simp_all
text {*
- For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text
+ For @{term "x ~= UU"} in assumptions @{text defined} replaces @{text
x} by @{text "Def a"} in conclusion. *}
-ML {*
- local val lift_definedE = thm "lift_definedE"
- in val def_tac = SIMPSET' (fn ss =>
- etac lift_definedE THEN' asm_simp_tac ss)
- end;
-*}
+method_setup defined = {*
+ Scan.succeed (fn ctxt => SIMPLE_METHOD'
+ (etac @{thm lift_definedE} THEN' asm_simp_tac (local_simpset_of ctxt)))
+*} ""
lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"
by simp