src/HOL/ex/Iff_Oracle.thy
changeset 42814 5af15f1e2ef6
parent 42361 23f352990944
child 50126 3dec88149176
     1.1 --- a/src/HOL/ex/Iff_Oracle.thy	Sun May 15 17:06:35 2011 +0200
     1.2 +++ b/src/HOL/ex/Iff_Oracle.thy	Sun May 15 17:45:53 2011 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4      SIMPLE_METHOD
     1.5        (HEADGOAL (rtac (iff_oracle (Proof_Context.theory_of ctxt, n)))
     1.6          handle Fail _ => no_tac))
     1.7 -*} "iff oracle"
     1.8 +*}
     1.9  
    1.10  
    1.11  lemma "A <-> A"