src/LCF/ex/Ex3.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/LCF/ex/Ex3.thy	Fri May 08 13:54:45 1998 +0200
@@ -0,0 +1,14 @@
+
+(*** Addition with fixpoint of successor ***)
+
+Ex3 = LCF +
+
+consts
+  s	:: "'a => 'a"
+  p	:: "'a => 'a => 'a"
+
+rules
+  p_strict	"p(UU) = UU"
+  p_s		"p(s(x),y) = s(p(x,y))"
+
+end