src/HOL/Hyperreal/Fact.thy
changeset 12196 a3be6b3a9c0b
child 15094 a7d1a3fdc30d
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/Fact.thy	Thu Nov 15 16:12:49 2001 +0100
@@ -0,0 +1,14 @@
+(*  Title       : Fact.thy 
+    Author      : Jacques D. Fleuriot
+    Copyright   : 1998  University of Cambridge
+    Description : Factorial function
+*)
+
+Fact = NatStar + 
+
+consts fact :: nat => nat 
+primrec 
+   fact_0     "fact 0 = 1"
+   fact_Suc   "fact (Suc n) = (Suc n) * fact n" 
+
+end
\ No newline at end of file