src/HOL/Recdef.thy
changeset 22399 80395c2c40cc
parent 22264 6a65e9b2ae05
child 22622 25693088396b
     1.1 --- a/src/HOL/Recdef.thy	Sat Mar 03 09:26:58 2007 +0100
     1.2 +++ b/src/HOL/Recdef.thy	Sat Mar 03 09:27:00 2007 +0100
     1.3 @@ -82,20 +82,4 @@
     1.4    wf_implies_wfP
     1.5    wfP_implies_wf
     1.6  
     1.7 -(* The following should really go into Datatype or Finite_Set, but
     1.8 -each one lacks the other theory as a parent . . . *)
     1.9 -
    1.10 -lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
    1.11 -by (rule set_ext, case_tac x, auto)
    1.12 -
    1.13 -instance option :: (finite) finite
    1.14 -proof
    1.15 -  have "finite (UNIV :: 'a set)" by (rule finite)
    1.16 -  hence "finite (insert None (Some ` (UNIV :: 'a set)))" by simp
    1.17 -  also have "insert None (Some ` (UNIV :: 'a set)) = UNIV"
    1.18 -    by (rule insert_None_conv_UNIV)
    1.19 -  finally show "finite (UNIV :: 'a option set)" .
    1.20 -qed
    1.21 -
    1.22 -
    1.23  end