Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Algebra/poly/UnivPoly2.thy
changeset 15596 8665d08085df
parent 15481 fc075ae929e4
child 16052 880b0e786c1b 
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Tue Mar 08 16:02:52 2005 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Mar 09 18:44:52 2005 +0100
@@ -249,7 +249,6 @@
 instance up :: (ring) ring
 proof
   fix p q r :: "'a::ring up"
-  fix n
   show "(p + q) + r = p + (q + r)"
     by (rule up_eqI) simp
   show "0 + p = p"
@@ -318,6 +317,7 @@
     by (simp add: up_inverse_def)
   show "p / q = p * inverse q"
     by (simp add: up_divide_def)
+  fix n
   show "p ^ n = nat_rec 1 (%u b. b * p) n"
     by (simp add: up_power_def)
   qed
isabelle