# HG changeset patch
# User haftmann
# Date 1172910420 -3600
# Node ID 80395c2c40cca291c5db74a0d3a292e62f419f59
# Parent  dfe146d65b14c8f4d434013b59e6f5cd4b454e19
moved instance option :: finite to Finite_Set.thy

diff -r dfe146d65b14 -r 80395c2c40cc src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Sat Mar 03 09:26:58 2007 +0100
+++ b/src/HOL/Recdef.thy	Sat Mar 03 09:27:00 2007 +0100
@@ -82,20 +82,4 @@
   wf_implies_wfP
   wfP_implies_wf
 
-(* The following should really go into Datatype or Finite_Set, but
-each one lacks the other theory as a parent . . . *)
-
-lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
-by (rule set_ext, case_tac x, auto)
-
-instance option :: (finite) finite
-proof
-  have "finite (UNIV :: 'a set)" by (rule finite)
-  hence "finite (insert None (Some ` (UNIV :: 'a set)))" by simp
-  also have "insert None (Some ` (UNIV :: 'a set)) = UNIV"
-    by (rule insert_None_conv_UNIV)
-  finally show "finite (UNIV :: 'a option set)" .
-qed
-
-
 end