# HG changeset patch
# User wenzelm
# Date 972292552 -7200
# Node ID a88d347db404157fe567b0d333746b0b5d04b477
# Parent  8018d1743bebc5e060880bb0f5070ab5fb2a75d4
isatool unsymbolize;

diff -r 8018d1743beb -r a88d347db404 src/HOL/subset.thy
--- a/src/HOL/subset.thy	Mon Oct 23 11:14:43 2000 +0200
+++ b/src/HOL/subset.thy	Mon Oct 23 11:15:52 2000 +0200
@@ -28,9 +28,9 @@
   -- {* This will be stated as an axiom for each typedef! *}
 
 lemma type_definitionI [intro]:
-  "(\<And>x. Rep x \<in> A) \<Longrightarrow>
-    (\<And>x. Abs (Rep x) = x) \<Longrightarrow>
-    (\<And>y. y \<in> A \<Longrightarrow> Rep (Abs y) = y) \<Longrightarrow>
+  "(!!x. Rep x \<in> A) ==>
+    (!!x. Abs (Rep x) = x) ==>
+    (!!y. y \<in> A ==> Rep (Abs y) = y) ==>
     type_definition Rep Abs A"
   by (unfold type_definition_def) blast