src/ZF/IMP/Equiv.thy

--- a/src/ZF/IMP/Equiv.thy	Tue Jun 06 19:24:05 2006 +0200
+++ b/src/ZF/IMP/Equiv.thy	Tue Jun 06 20:42:25 2006 +0200
@@ -69,7 +69,7 @@
    apply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption)
    apply (unfold Gamma_def)
    apply force
-  txt {* @{text if} *}
+  txt {* @{text "if"} *}
   apply auto
   done