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/Word/WordGenLib.thy
changeset 35416 d8d7d1b785af
parent 30729 461ee3e49ad3 
--- a/src/HOL/Word/WordGenLib.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Word/WordGenLib.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -344,8 +344,7 @@
   apply (case_tac "1+n = 0", auto)
   done
 
-constdefs
-  word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
+definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a" where
   "word_rec forZero forSuc n \<equiv> nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
 
 lemma word_rec_0: "word_rec z s 0 = z"
isabelle