# HG changeset patch
# User krauss
# Date 1193243573 -7200
# Node ID bd06fd396fd0f357af69aad5dfa5044d71a7586c
# Parent  b1ea9d2e6a72bfb890c2557ef17d6b04c1024f1d
tuned

diff -r b1ea9d2e6a72 -r bd06fd396fd0 src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Wed Oct 24 18:30:06 2007 +0200
+++ b/src/HOL/ex/Fundefs.thy	Wed Oct 24 18:32:53 2007 +0200
@@ -31,7 +31,7 @@
 
 subsection {* Currying *}
 
-fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+fun add
 where
   "add 0 y = y"
 | "add (Suc x) y = Suc (add x y)"
@@ -42,7 +42,7 @@
 
 subsection {* Nested recursion *}
 
-function nz :: "nat \<Rightarrow> nat"
+function nz 
 where
   "nz 0 = 0"
 | "nz (Suc x) = nz (nz x)"
@@ -182,9 +182,6 @@
 assumes assoc: "opr (opr x y) z = opr x (opr y z)"
   and lunit: "opr un x = x"
   and runit: "opr x un = x"
-
-
-context my_monoid
 begin
 
 fun foldR :: "'a list \<Rightarrow> 'a"
@@ -362,7 +359,7 @@
   f4 :: "nat \<Rightarrow> nat \<Rightarrow> bool" 
 where
   "f4 0 0 = True"
-| "f4 x y = False"
+| "f4 _ _ = False"
 
 
 end