# HG changeset patch
# User nipkow
# Date 1101723828 -3600
# Node ID a7b603bbc1e697db450a444ff7a3c3d46428620d
# Parent  08519594b0e46e1ffec7903c3469b71602daaf4f
onsolete

diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/Ackermann.thy
--- a/doc-src/Tutorial/Misc/Ackermann.thy	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-Ackermann = WF_Rel +
-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))"
-end
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/Chain.thy
--- a/doc-src/Tutorial/Misc/Chain.thy	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-Chain = List +
-consts chain :: "('a => 'a => bool) * 'a list => bool"
-recdef chain "measure (%(r,xs). length xs)"
-    "chain(r, [])     = True"
-    "chain(r, [x])    = True"
-    "chain(r, x#y#zs) = (r x y & chain(r, y#zs))"
-end
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/ConstDefs.thy
--- a/doc-src/Tutorial/Misc/ConstDefs.thy	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-ConstDefs = Types +
-constdefs nand :: gate
-         "nand A B == ~(A & B)"
-          exor :: gate
-         "exor A B == A & ~B | ~A & B"
-end
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/Defs.thy
--- a/doc-src/Tutorial/Misc/Defs.thy	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-Defs = Types +
-consts nand, exor :: gate
-defs nand_def "nand A B == ~(A & B)"
-     exor_def "exor A B == A & ~B | ~A & B"
-end
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/Exor.thy
--- a/doc-src/Tutorial/Misc/Exor.thy	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-Exor = Main +
-constdefs
- exor :: bool => bool => bool
-"exor A B == (A & ~B) | (~A & B)"
-end
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/Fib.thy
--- a/doc-src/Tutorial/Misc/Fib.thy	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-Fib = WF_Rel +
-consts fib  :: nat => nat
-recdef fib "measure(%n. n)"
-    "fib 0 = 0"
-    "fib 1 = 1"
-    "fib (Suc(Suc x)) = fib x + fib (Suc x)"
-end
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/GCD.ML
--- a/doc-src/Tutorial/Misc/GCD.ML	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-Goal "gcd(m,0) = m";
-by(resolve_tac [trans] 1);
-by(resolve_tac gcd.rules 1);
-by(Simp_tac 1);
-qed "gcd_0";
-Addsimps [gcd_0];
-
-Goal "!!n. n ~= 0 ==> gcd(m,n) = gcd(n, m mod n)";
-by(resolve_tac [trans] 1);
-by(resolve_tac gcd.rules 1);
-by(Asm_simp_tac 1);
-qed "gcd_not_0";
-Addsimps [gcd_not_0];
-
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/GCD.thy
--- a/doc-src/Tutorial/Misc/GCD.thy	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-GCD = WF_Rel +
-consts gcd :: "nat*nat => nat"
-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))"
-end
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/InfixTree.ML
--- a/doc-src/Tutorial/Misc/InfixTree.ML	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-Goal "!xs. linInfixList t xs = infixList t @ xs";
-by(induct_tac "t" 1);
-by(Simp_tac 1);
-by(Asm_simp_tac 1);
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/Itrev.thy
--- a/doc-src/Tutorial/Misc/Itrev.thy	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-Itrev = Main +
-consts itrev :: 'a list => 'a list => 'a list
-primrec
-"itrev []     ys = ys"
-"itrev (x#xs) ys = itrev xs (x#ys)"
-end
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/Last.thy
--- a/doc-src/Tutorial/Misc/Last.thy	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-Last = List +
-consts last :: 'a list => 'a
-recdef last "measure (%xs. length xs)"
-    "last [x]      = x"
-    "last (x#y#zs) = last (y#zs)"
-end
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/NatSum.ML
--- a/doc-src/Tutorial/Misc/NatSum.ML	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-Goal "sum n + sum n = n*(Suc n)";
-by(induct_tac "n" 1);
-by(Auto_tac);
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/NatSum.thy
--- a/doc-src/Tutorial/Misc/NatSum.thy	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-NatSum = Main +
-consts sum :: nat => nat
-primrec
-"sum 0 = 0"
-"sum (Suc n) = Suc n + sum n"
-end
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/ROOT.ML
--- a/doc-src/Tutorial/Misc/ROOT.ML	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-context Main.thy;
-use "arith1.ML";
-by(Auto_tac);
-use "arith2.ML";
-by(arith_tac 1);
-use "arith3.ML";
-by(arith_tac 1);
-
-use_thy "Tree";
-
-context Main.thy;
-use"exhaust.ML";
-use"autotac.ML";
-result();
-
-use_thy"NatSum";
-result();
-
-use_thy"Types";
-use_thy"Defs";
-use_thy"ConstDefs";
-
-context Main.thy;
-Goal "! xs. if xs = [] then rev xs = [] else rev xs ~= []";
-use"splitif.ML";
-
-Goal "(case xs of [] => zs | y#ys => y#(ys@zs)) = xs@zs";
-use"splitlist.ML";
-
-use_thy "Itrev";
-use "itrev1.ML";
-use "itrev2.ML";
-use "itrev3.ML";
-use "induct_auto.ML";
-result();
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/Sep.thy
--- a/doc-src/Tutorial/Misc/Sep.thy	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-Sep = List +
-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)"
-end
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/Sep2.thy
--- a/doc-src/Tutorial/Misc/Sep2.thy	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-Sep2 = List +
-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 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/Tree.thy
--- a/doc-src/Tutorial/Misc/Tree.thy	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-Tree = Main +
-datatype 'a tree = Tip | Node ('a tree) 'a ('a tree)
-end
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/Types.thy
--- a/doc-src/Tutorial/Misc/Types.thy	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-Types = Main +
-types number       = nat
-      gate         = bool => bool => bool
-      ('a,'b)alist = "('a * 'b)list"
-end
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/arith1.ML
--- a/doc-src/Tutorial/Misc/arith1.ML	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-Goal "[| ~ m < n; m < n+1 |] ==> m = n";
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/arith2.ML
--- a/doc-src/Tutorial/Misc/arith2.ML	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-Goal "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/arith3.ML
--- a/doc-src/Tutorial/Misc/arith3.ML	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-Goal "~ m < n & m < n+1 ==> m = n";
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/autotac.ML
--- a/doc-src/Tutorial/Misc/autotac.ML	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-by(Auto_tac);
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/constdefs
--- a/doc-src/Tutorial/Misc/constdefs	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-constdefs nand :: gate
-         "nand A B == ~(A & B)"
-          exor :: gate
-         "exor A B == A & ~B | ~A & B"
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/constdefsprolog
--- a/doc-src/Tutorial/Misc/constdefsprolog	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-ConstDefs = Types +
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/consts
--- a/doc-src/Tutorial/Misc/consts	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-consts nand, exor :: gate
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/defs
--- a/doc-src/Tutorial/Misc/defs	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-defs nand_def "nand A B == ~(A & B)"
-     exor_def "exor A B == A & ~B | ~A & B"
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/defsprolog
--- a/doc-src/Tutorial/Misc/defsprolog	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-Defs = Types +
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/end
--- a/doc-src/Tutorial/Misc/end	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-end
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/exhaust.ML
--- a/doc-src/Tutorial/Misc/exhaust.ML	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-Goal "(case xs of [] => [] | y#ys => xs) = xs";
-by(case_tac "xs" 1);
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/exorgoal.ML
--- a/doc-src/Tutorial/Misc/exorgoal.ML	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-Goalw [exor_def] "exor A (~A)";
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/exorproof.ML
--- a/doc-src/Tutorial/Misc/exorproof.ML	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-by(simp_tac (simpset() addsimps [exor_def]) 1);
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/induct_auto.ML
--- a/doc-src/Tutorial/Misc/induct_auto.ML	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-by(induct_tac "xs" 1);
-by(Auto_tac);
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/itrev1.ML
--- a/doc-src/Tutorial/Misc/itrev1.ML	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-Goal "itrev xs [] = rev xs";
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/itrev2.ML
--- a/doc-src/Tutorial/Misc/itrev2.ML	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-Goal "itrev xs ys = rev xs @ ys";
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/itrev3.ML
--- a/doc-src/Tutorial/Misc/itrev3.ML	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-Goal "!ys. itrev xs ys = rev xs @ ys";
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/natsum
--- a/doc-src/Tutorial/Misc/natsum	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-consts sum :: nat => nat
-primrec
-"sum 0 = 0"
-"sum (Suc n) = Suc n + sum n"
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/natsumprolog
--- a/doc-src/Tutorial/Misc/natsumprolog	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-NatSum = Main +
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/splitif.ML
--- a/doc-src/Tutorial/Misc/splitif.ML	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-by(split_tac [split_if] 1);
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/splitlist.ML
--- a/doc-src/Tutorial/Misc/splitlist.ML	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-by(split_tac [list.split] 1);
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/tree
--- a/doc-src/Tutorial/Misc/tree	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-datatype 'a tree = Tip | Node ('a tree) 'a ('a tree)
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/treeprolog
--- a/doc-src/Tutorial/Misc/treeprolog	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-Tree = Main +
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/types
--- a/doc-src/Tutorial/Misc/types	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-types number       = nat
-      gate         = bool => bool => bool
-      ('a,'b)alist = "('a * 'b)list"
diff -r 08519594b0e4 -r a7b603bbc1e6 doc-src/Tutorial/Misc/typesprolog
--- a/doc-src/Tutorial/Misc/typesprolog	Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-Types = Main +