# HG changeset patch
# User haftmann
# Date 1199520987 -3600
# Node ID f7771e4f7064bd14c115c2d5fa3bc93bf2539efe
# Parent  5dac4855a080672508791a8989aa67a52ee84c92
more instantiation

diff -r 5dac4855a080 -r f7771e4f7064 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Sat Jan 05 09:16:11 2008 +0100
+++ b/src/HOL/Datatype.thy	Sat Jan 05 09:16:27 2008 +0100
@@ -610,8 +610,13 @@
 lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
   by (rule set_ext, case_tac x) auto
 
-instance option :: (finite) finite
-proof
+instantiation option :: (finite) finite
+begin
+
+definition
+  "Finite_Set.itself = TYPE('a option)"
+
+instance 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"
@@ -619,6 +624,8 @@
   finally show "finite (UNIV :: 'a option set)" .
 qed
 
+end
+
 lemma univ_option [noatp, code func]:
   "UNIV = insert (None \<Colon> 'a\<Colon>finite option) (image Some UNIV)"
   unfolding insert_None_conv_UNIV ..
diff -r 5dac4855a080 -r f7771e4f7064 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Sat Jan 05 09:16:11 2008 +0100
+++ b/src/HOL/Power.thy	Sat Jan 05 09:16:27 2008 +0100
@@ -323,19 +323,21 @@
 
 subsection{*Exponentiation for the Natural Numbers*}
 
-instance nat :: power ..
+instantiation nat :: recpower
+begin
 
-primrec (power)
-  "p ^ 0 = 1"
-  "p ^ (Suc n) = (p::nat) * (p ^ n)"
+primrec power_nat where
+  "p ^ 0 = (1\<Colon>nat)"
+  | "p ^ (Suc n) = (p\<Colon>nat) * (p ^ n)"
 
-instance nat :: recpower
-proof
+instance proof
   fix z n :: nat
   show "z^0 = 1" by simp
   show "z^(Suc n) = z * (z^n)" by simp
 qed
 
+end
+
 lemma of_nat_power:
   "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
 by (induct n, simp_all add: power_Suc of_nat_mult)