Remove some HOL88 quoting from a .doc file

help/Docfiles/reduceLib.IMP_CONV.doc

@@ -13,26 +13,26 @@ term of type {bool}, then {IMP_CONV tm} returns the corresponding theorem. Note
 that in the last case the antecedent and consequent need only be
 alpha-equivalent rather than strictly identical.
 {
-   IMP_CONV "T ==> t" = |- T ==> t = t
-   IMP_CONV "t ==> T" = |- t ==> T = T
-   IMP_CONV "F ==> t" = |- F ==> t = T
-   IMP_CONV "t ==> F" = |- t ==> F = ~t
-   IMP_CONV "t ==> t" = |- t ==> t = T
+   IMP_CONV “T ==> t” = |- T ==> t = t
+   IMP_CONV “t ==> T” = |- t ==> T = T
+   IMP_CONV “F ==> t” = |- F ==> t = T
+   IMP_CONV “t ==> F” = |- t ==> F = ~t
+   IMP_CONV “t ==> t” = |- t ==> t = T
 }
 
 \FAILURE
 {IMP_CONV tm} fails unless {tm} has one of the forms indicated above.
 
 \EXAMPLE
 {
-#IMP_CONV "T ==> F";;
-|- T ==> F = F
+> IMP_CONV “T ==> F”;
+val it =  ⊢ T ⇒ F ⇔ F : thm
 
-#IMP_CONV "F ==> x";;
-|- F ==> x = T
+> IMP_CONV “F ==> x”;
+val it = ⊢ F ⇒ x ⇔ T : thm
 
-#IMP_CONV "(!z:(num)list. z = z) ==> (!x:(num)list. x = x)";;
-|- (!z. z = z) ==> (!x. x = x) = T
+> IMP_CONV “(!z:(num)list. z = z) ==> (!x:(num)list. x = x)”;
+val it =  ⊢ (∀z. z = z) ⇒ (∀z. z = z) ⇔ T : thm
 }
 
 \ENDDOC