Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Sequents/LK.thy
changeset 45602 2a858377c3d2
parent 42795 66fcc9882784
child 48891 c0eafbd55de3 
--- a/src/Sequents/LK.thy	Sun Nov 20 17:57:09 2011 +0100
+++ b/src/Sequents/LK.thy	Sun Nov 20 20:15:02 2011 +0100
@@ -129,14 +129,14 @@
   apply (tactic {* fast_tac LK_pack 1 *})
   done
 
-lemmas iff_reflection_F = P_iff_F [THEN iff_reflection, standard]
+lemmas iff_reflection_F = P_iff_F [THEN iff_reflection]
 
 lemma P_iff_T: "|- P ==> |- (P <-> True)"
   apply (erule thinR [THEN cut])
   apply (tactic {* fast_tac LK_pack 1 *})
   done
 
-lemmas iff_reflection_T = P_iff_T [THEN iff_reflection, standard]
+lemmas iff_reflection_T = P_iff_T [THEN iff_reflection]
 
 
 lemma LK_extra_simps:
isabelle