# HG changeset patch
# User paulson
# Date 865585160 -7200
# Node ID f060dc3f15a81c9817e7a6c2583eb32515dd3966
# Parent  58ccb80eb50aa58232f95c07922304fd059073d2
Two new examples; corrected a comment

diff -r 58ccb80eb50a -r f060dc3f15a8 src/HOL/ex/Recdef.thy
--- a/src/HOL/ex/Recdef.thy	Fri Jun 06 10:18:46 1997 +0200
+++ b/src/HOL/ex/Recdef.thy	Fri Jun 06 10:19:20 1997 +0200
@@ -8,8 +8,16 @@
 
 Recdef = WF_Rel + List +
 
+consts fact :: "nat => nat"
+recdef fact "less_than"
+    "fact x = (if (x = 0) then 1 else x * fact (x - 1))"
+
+consts Fact :: "nat => nat"
+recdef Fact "less_than"
+    "Fact 0 = 1"
+    "Fact (Suc x) = (Fact x * Suc x)"
+
 consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list"
-
 recdef map2 "measure(%(f,l1,l2).size l1)"
     "map2(f, [], [])  = []"
     "map2(f, h#t, []) = []"
@@ -42,7 +50,7 @@
     "gcd (Suc x, Suc y) = (if (y <= x) then gcd(x - y, Suc y)  
                                        else gcd(Suc x, y - x))"
 
-(*Not handled automatically.  In fact, g is the identity function.*)
+(*Not handled automatically.  In fact, g is the zero constant function.*)
 consts g   :: "nat => nat"
 recdef g "less_than"
     "g 0 = 0"