src/HOL/HOLCF/Lift.thy
changeset 42814 5af15f1e2ef6
parent 42151 4da4fc77664b
child 49759 ecf1d5d87e5e
     1.1 --- a/src/HOL/HOLCF/Lift.thy	Sun May 15 17:06:35 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Lift.thy	Sun May 15 17:45:53 2011 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4  method_setup defined = {*
     1.5    Scan.succeed (fn ctxt => SIMPLE_METHOD'
     1.6      (etac @{thm lift_definedE} THEN' asm_simp_tac (simpset_of ctxt)))
     1.7 -*} ""
     1.8 +*}
     1.9  
    1.10  lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"
    1.11    by simp