--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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];
-
--- 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
--- 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);
--- 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
--- 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
--- 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);
--- 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
--- 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();
--- 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
--- 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
--- 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
--- 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
--- 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";
--- 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))";
--- 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";
--- 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);
--- 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"
--- 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 +
--- 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
--- 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"
--- 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 +
--- 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
--- 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);
--- 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)";
--- 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);
--- 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);
--- 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";
--- 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";
--- 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";
--- 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"
--- 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 +
--- 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);
--- 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);
--- 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)
--- 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 +
--- 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"
--- 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 +