# HG changeset patch
# User nipkow
# Date 916152553 -3600
# Node ID 40d66bc3e83f845bce5a621e4fb3ad177003d48b
# Parent  d4866f6ff2f9336ba14e1acf44b5e72d950ca319
*** empty log message ***

diff -r d4866f6ff2f9 -r 40d66bc3e83f doc-src/Tutorial/Recdef/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Recdef/ROOT.ML	Tue Jan 12 15:49:13 1999 +0100
@@ -0,0 +1,5 @@
+use_thy "Examples";
+gcd.rules;
+use_thy "Sep1";
+use_thy "Sep2";
+(* test *)
diff -r d4866f6ff2f9 -r 40d66bc3e83f doc-src/Tutorial/Recdef/Sep1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Recdef/Sep1.thy	Tue Jan 12 15:49:13 1999 +0100
@@ -0,0 +1,6 @@
+Sep1 = Main +
+consts sep :: "'a * 'a list => 'a list"
+recdef sep "measure (%(a,xs). length xs)"
+  "sep(a, x#y#zs) = x # a # sep(a,y#zs)"
+  "sep(a, xs)     = xs"
+end
diff -r d4866f6ff2f9 -r 40d66bc3e83f doc-src/Tutorial/Recdef/Sep2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Recdef/Sep2.thy	Tue Jan 12 15:49:13 1999 +0100
@@ -0,0 +1,6 @@
+Sep2 = Main +
+consts sep :: 'a list => 'a => 'a list
+recdef sep "measure length"
+  "sep (x#y#zs) = (%a. x # a # sep zs a)"
+  "sep xs       = (%a. xs)"
+end
diff -r d4866f6ff2f9 -r 40d66bc3e83f doc-src/Tutorial/Recdef/ack
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Recdef/ack	Tue Jan 12 15:49:13 1999 +0100
@@ -0,0 +1,5 @@
+consts ack :: "nat*nat => nat"
+recdef ack "measure(%m. m) ** measure(%n. n)"
+  "ack(0,n)         = Suc n"
+  "ack(Suc m,0)     = ack(m, 1)"
+  "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))"
diff -r d4866f6ff2f9 -r 40d66bc3e83f doc-src/Tutorial/Recdef/constsgcd
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Recdef/constsgcd	Tue Jan 12 15:49:13 1999 +0100
@@ -0,0 +1,1 @@
+consts gcd :: "nat*nat => nat"
diff -r d4866f6ff2f9 -r 40d66bc3e83f doc-src/Tutorial/Recdef/end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Recdef/end	Tue Jan 12 15:49:13 1999 +0100
@@ -0,0 +1,1 @@
+end
diff -r d4866f6ff2f9 -r 40d66bc3e83f doc-src/Tutorial/Recdef/exprolog
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Recdef/exprolog	Tue Jan 12 15:49:13 1999 +0100
@@ -0,0 +1,1 @@
+Examples = Main +
diff -r d4866f6ff2f9 -r 40d66bc3e83f doc-src/Tutorial/Recdef/fib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Recdef/fib	Tue Jan 12 15:49:13 1999 +0100
@@ -0,0 +1,5 @@
+consts fib :: nat => nat
+recdef fib "measure(%n. n)"
+  "fib 0 = 0"
+  "fib 1 = 1"
+  "fib (Suc(Suc x)) = fib x + fib (Suc x)"
diff -r d4866f6ff2f9 -r 40d66bc3e83f doc-src/Tutorial/Recdef/gcd
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Recdef/gcd	Tue Jan 12 15:49:13 1999 +0100
@@ -0,0 +1,3 @@
+recdef gcd "measure ((%(m,n).n))"
+  simpset "simpset() addsimps [mod_less_divisor]"
+  "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
diff -r d4866f6ff2f9 -r 40d66bc3e83f doc-src/Tutorial/Recdef/last
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Recdef/last	Tue Jan 12 15:49:13 1999 +0100
@@ -0,0 +1,4 @@
+consts last :: 'a list => 'a
+recdef last "measure (%xs. length xs)"
+  "last [x]      = x"
+  "last (x#y#zs) = last (y#zs)"
diff -r d4866f6ff2f9 -r 40d66bc3e83f doc-src/Tutorial/Recdef/sep
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Recdef/sep	Tue Jan 12 15:49:13 1999 +0100
@@ -0,0 +1,5 @@
+consts sep :: "'a * 'a list => 'a list"
+recdef sep "measure (%(a,xs). length xs)"
+  "sep(a, [])     = []"
+  "sep(a, [x])    = [x]"
+  "sep(a, x#y#zs) = x # a # sep(a,y#zs)"
diff -r d4866f6ff2f9 -r 40d66bc3e83f doc-src/Tutorial/Recdef/sep1
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Recdef/sep1	Tue Jan 12 15:49:13 1999 +0100
@@ -0,0 +1,3 @@
+recdef sep "measure (%(a,xs). length xs)"
+  "sep(a, x#y#zs) = x # a # sep(a,y#zs)"
+  "sep(a, xs)     = xs"
diff -r d4866f6ff2f9 -r 40d66bc3e83f doc-src/Tutorial/Recdef/sep1prolog
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Recdef/sep1prolog	Tue Jan 12 15:49:13 1999 +0100
@@ -0,0 +1,2 @@
+Sep1 = Main +
+consts sep :: "'a * 'a list => 'a list"
diff -r d4866f6ff2f9 -r 40d66bc3e83f doc-src/Tutorial/Recdef/sep2
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Recdef/sep2	Tue Jan 12 15:49:13 1999 +0100
@@ -0,0 +1,4 @@
+consts sep :: 'a list => 'a => 'a list
+recdef sep "measure length"
+  "sep (x#y#zs) = (%a. x # a # sep zs a)"
+  "sep xs       = (%a. xs)"
diff -r d4866f6ff2f9 -r 40d66bc3e83f doc-src/Tutorial/Recdef/sep2prolog
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Recdef/sep2prolog	Tue Jan 12 15:49:13 1999 +0100
@@ -0,0 +1,1 @@
+Sep2 = Main +