# HG changeset patch
# User wenzelm
# Date 972292483 -7200
# Node ID 8018d1743bebc5e060880bb0f5070ab5fb2a75d4
# Parent  475ea668c67d148580f456f7909755ed8f56ba8c
added type_definitionI;

diff -r 475ea668c67d -r 8018d1743beb src/HOL/subset.thy
--- a/src/HOL/subset.thy	Mon Oct 23 11:14:00 2000 +0200
+++ b/src/HOL/subset.thy	Mon Oct 23 11:14:43 2000 +0200
@@ -27,6 +27,13 @@
     (\<forall>y \<in> A. Rep (Abs y) = y)"
   -- {* 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>
+    type_definition Rep Abs A"
+  by (unfold type_definition_def) blast
+
 theorem Rep: "type_definition Rep Abs A ==> Rep x \<in> A"
   by (unfold type_definition_def) blast