# HG changeset patch
# User nipkow
# Date 904145247 -7200
# Node ID efb799c5ed3c17faaf5050eb9b802cf9655b13ba
# Parent  60b31a24f1a6e104ffb96f800bb29e5097bbc4a6
*** empty log message ***

diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/CodeGen/CodeGen.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/CodeGen.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,26 @@
+CodeGen = Main +
+types 'v binop = 'v => 'v => 'v
+datatype ('a,'v) expr = Cex 'v
+                      | Vex 'a
+                      | Bex ('v binop)  (('a,'v) expr) (('a,'v) expr)
+consts value :: ('a => 'v) => ('a,'v)expr => 'v
+primrec
+"value env (Cex v) = v"
+"value env (Vex a) = env a"
+"value env (Bex f e1 e2) = f (value env e1) (value env e2)"
+datatype ('a,'v) instr = Const 'v
+                       | Load 'a
+                       | Apply ('v binop)
+consts exec :: ('a => 'v) => 'v list => (('a,'v) instr) list => 'v list
+primrec
+"exec s vs [] = vs"
+"exec s vs (i#is) = (case i of
+    Const v  => exec s (v#vs) is
+  | Load a   => exec s ((s a)#vs) is
+  | Apply f  => exec s ( (f (hd vs) (hd(tl vs)))#(tl(tl vs)) ) is)"
+consts comp :: ('a,'v) expr => (('a,'v) instr) list
+primrec
+"comp (Cex v)       = [Const v]"
+"comp (Vex a)       = [Load a]"
+"comp (Bex f e1 e2) = (comp e2) @ (comp e1) @ [Apply f]"
+end
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/CodeGen/CodeGenIf.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/CodeGenIf.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,39 @@
+Addsimps exec.rules;
+Addsimps [Let_def,drop_all];
+Addsplits [split_instr_case];
+
+Goal "!xs. wf xs --> wf(drop n xs)";
+by(induct_tac "n" 1);
+by(Simp_tac 1);
+by(Clarify_tac 1);
+by(exhaust_tac "xs" 1);
+by(Asm_simp_tac 1);
+by(Asm_full_simp_tac 1);
+qed_spec_mp "wf_drop";
+Addsimps [wf_drop];
+
+Goal "wf xs --> wf ys --> wf(xs@ys)";
+by(induct_tac "xs" 1);
+by(Simp_tac 1);
+by(asm_full_simp_tac (simpset() addsimps [trans_le_add1]) 1);
+qed_spec_mp "wf_append";
+Addsimps [wf_append];
+
+Goal "!vs ys. wf xs --> exec(s,vs,xs@ys) = exec(s,exec(s,vs,xs),ys)"; 
+by(res_inst_tac [("xs","xs")] length_induct 1);
+by(exhaust_tac "xs" 1);
+by(Asm_full_simp_tac 1);
+by(asm_full_simp_tac (simpset() addsimps [less_imp_diff_is_0,diff_less_Suc,le_imp_less_Suc]) 1);
+qed_spec_mp "exec_append";
+Addsimps [exec_append];
+
+Goal "wf(comp e)";
+by(induct_tac "e" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "wf_comp";
+Addsimps [wf_comp];
+
+Goal "!vs. exec(s, vs, comp e) = (value s e) # vs";
+by(induct_tac "e" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "exec_comp";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/CodeGen/CodeGenIf.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/CodeGenIf.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,46 @@
+CodeGenIf = List +
+types 'v binop = 'v => 'v => 'v
+      'v test = 'v => bool
+datatype ('a,'v) expr = Vex 'a 
+                      | Cex 'v
+                      | Bex ('v binop) (('a,'v) expr) (('a,'v) expr)
+                      | Ifex ('v test) (('a,'v)expr) (('a,'v)expr) (('a,'v)expr)
+consts value :: ('a => 'v) => ('a,'v)expr => 'v
+primrec value expr
+"value env (Vex a) = env a"
+"value env (Cex v) = v"
+"value env (Bex f e1 e2) = f (value env e1) (value env e2)"
+"value env (Ifex t b e1 e2) =
+   (if t(value env b) then value env e1 else value env e2)"
+datatype ('a,'v) instr = Load 'a
+                       | Const 'v
+                       | Apply ('v binop)
+                       | Jump nat
+                       | Test ('v test) nat
+consts exec :: "('a => 'v) * 'v list * (('a,'v) instr) list => 'v list"
+recdef exec "measure(%(s,vs,is).length is)"
+simpset "simpset() addsimps [diff_less_Suc]"
+"exec(s, vs, []) = vs"
+"exec(s, vs, i#is) = (case i of
+    Load a   => exec(s,(s a)#vs,is)
+  | Const v  => exec(s,v#vs,is)
+  | Apply f  => exec(s, (f (hd vs) (hd(tl vs)))#(tl(tl vs)), is)
+  | Jump n   => exec(s, vs, drop n is)
+  | Test t n => (if t(hd vs) then exec(s,tl vs, drop n is)
+                             else exec(s,tl vs, is)))"
+consts comp :: ('a,'v) expr => (('a,'v) instr) list
+primrec comp expr
+"comp (Vex a) = [Load a]"
+"comp (Cex v) = [Const v]"
+"comp (Bex f e1 e2) = (comp e2)@(comp e1)@[Apply f]"
+"comp (Ifex t b e1 e2) = (let is1 = comp e1; is2 = comp e2
+                          in comp b @ [Test t (Suc(length is2))] @
+                             is2 @ [Jump (length is1)] @ is1)"
+
+consts wf :: ('a,'v)instr list => bool
+primrec wf list
+"wf [] = True"
+"wf (i#is) = (wf is & (case i of Load a => True | Const v => True
+  | Apply f  => True | Jump n => n <= length is | Test t n => n <= length is))"
+
+end
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/CodeGen/Lemma.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/Lemma.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Lemma = List
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/CodeGen/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/ROOT.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,13 @@
+use_thy"CodeGen";
+
+use"goal1.ML";
+by(induct_tac "xs" 1);
+by(Simp_tac 1);
+use"simpsplit.ML";
+qed "exec_append";
+Addsimps [exec_append];
+
+use"goal2.ML";
+by(induct_tac "e" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "exec_comp";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/CodeGen/comp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/comp	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,5 @@
+consts comp :: ('a,'v) expr => (('a,'v) instr) list
+primrec
+"comp (Cex v)       = [Const v]"
+"comp (Vex a)       = [Load a]"
+"comp (Bex f e1 e2) = (comp e2) @ (comp e1) @ [Apply f]"
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/CodeGen/end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/end	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+end
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/CodeGen/exec
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/exec	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,7 @@
+consts exec :: ('a => 'v) => 'v list => (('a,'v) instr) list => 'v list
+primrec
+"exec s vs [] = vs"
+"exec s vs (i#is) = (case i of
+    Const v  => exec s (v#vs) is
+  | Load a   => exec s ((s a)#vs) is
+  | Apply f  => exec s ( (f (hd vs) (hd(tl vs)))#(tl(tl vs)) ) is)"
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/CodeGen/expr
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/expr	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,4 @@
+types 'v binop = 'v => 'v => 'v
+datatype ('a,'v) expr = Cex 'v
+                      | Vex 'a
+                      | Bex ('v binop)  (('a,'v) expr) (('a,'v) expr)
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/CodeGen/goal1.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/goal1.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "!vs. exec s vs (xs@ys) = exec s (exec s vs xs) ys"; 
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/CodeGen/goal2.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/goal2.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "!vs. exec s vs (comp e) = (value s e) # vs";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/CodeGen/instr
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/instr	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,3 @@
+datatype ('a,'v) instr = Const 'v
+                       | Load 'a
+                       | Apply ('v binop)
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/CodeGen/prolog
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/prolog	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+CodeGen = Main +
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/CodeGen/simpsplit.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/simpsplit.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+by(asm_simp_tac (simpset() addsplits [instr.split]) 1);
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/CodeGen/value
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/value	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,5 @@
+consts value :: ('a => 'v) => ('a,'v)expr => 'v
+primrec
+"value env (Cex v) = v"
+"value env (Vex a) = env a"
+"value env (Bex f e1 e2) = f (value env e1) (value env e2)"
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/Exercise.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/Exercise.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,17 @@
+use "normif.ML";
+use "proof.ML";
+qed_spec_mp "normif_correct";
+Addsimps [normif_correct];
+
+use "norm.ML";
+use "proof.ML";
+qed "norm_correct";
+
+Goal "!t e. normal t & normal e --> normal(normif b t e)";
+use "proof.ML";
+qed_spec_mp "normal_normif";
+Addsimps [normal_normif];
+
+use "normal_norm.ML";
+use "proof.ML";
+qed "normal_norm";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/Exercise.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/Exercise.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,25 @@
+Exercise = Main +
+datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex
+consts valif :: ifex => (nat => bool) => bool
+primrec valif ifex
+"valif (CIF b)    env = b"
+"valif (VIF x)    env = env x"
+"valif (IF b t e) env = (if valif b env then valif t env
+                                        else valif e env)"
+consts normif :: ifex => ifex => ifex => ifex
+primrec normif ifex
+"normif (CIF b)    t e = (if b then t else e)"
+"normif (VIF x)    t e = IF (VIF x) t e"
+"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"
+consts norm :: ifex => ifex
+primrec norm ifex
+"norm (CIF b)    = CIF b"
+"norm (VIF x)    = VIF x"
+"norm (IF b t e) = normif b (norm t) (norm e)"
+consts normal :: ifex => bool
+primrec normal ifex
+"normal(CIF b) = True"
+"normal(VIF x) = True"
+"normal(IF b t e) = (normal t & normal e &
+      (case b of CIF b => False | VIF x => True | IF x y z => False))"
+end
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/Ifexpr.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/Ifexpr.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,21 @@
+use "bool2if.ML";
+use "proof.ML";
+qed "bool2if_correct";
+
+use "normif.ML";
+use "proof.ML";
+qed_spec_mp "normif_correct";
+Addsimps [normif_correct];
+
+use "norm.ML";
+use "proof.ML";
+qed "norm_correct";
+
+use "normal_normif.ML";
+use "proof.ML";
+qed_spec_mp "normal_normif";
+Addsimps [normal_normif];
+
+use "normal_norm.ML";
+use "proof.ML";
+qed "normal_norm";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/Ifexpr.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/Ifexpr.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,39 @@
+Ifexpr = Main +
+datatype boolex = Const bool | Var nat
+                | Neg boolex | And boolex boolex
+consts value :: boolex => (nat => bool) => bool
+primrec
+"value (Const b) env = b"
+"value (Var x)   env = env x"
+"value (Neg b)   env = (~ value b env)"
+"value (And b c) env = (value b env & value c env)"
+datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex
+consts valif :: ifex => (nat => bool) => bool
+primrec
+"valif (CIF b)    env = b"
+"valif (VIF x)    env = env x"
+"valif (IF b t e) env = (if valif b env then valif t env
+                                        else valif e env)"
+consts bool2if :: boolex => ifex
+primrec
+"bool2if (Const b) = CIF b"
+"bool2if (Var x)   = VIF x"
+"bool2if (Neg b)   = IF (bool2if b) (CIF False) (CIF True)"
+"bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)"
+consts normif :: ifex => ifex => ifex => ifex
+primrec
+"normif (CIF b)    t e = IF (CIF b) t e"
+"normif (VIF x)    t e = IF (VIF x) t e"
+"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"
+consts norm :: ifex => ifex
+primrec
+"norm (CIF b)    = CIF b"
+"norm (VIF x)    = VIF x"
+"norm (IF b t e) = normif b (norm t) (norm e)"
+consts normal :: ifex => bool
+primrec
+"normal(CIF b) = True"
+"normal(VIF x) = True"
+"normal(IF b t e) = (normal t & normal e &
+      (case b of CIF b => True | VIF x => True | IF x y z => False))"
+end
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/Makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/Makefile	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,3 @@
+
+Ifexpr.thy: prolog boolex value ifex valif bool2if normif norm normal end
+	cat prolog boolex value ifex valif bool2if normif norm normal end > Ifexpr.thy
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/ROOT.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+use_thy "Ifexpr";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/bool2if
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/bool2if	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+consts bool2if :: boolex => ifex
+primrec
+"bool2if (Const b) = CIF b"
+"bool2if (Var x)   = VIF x"
+"bool2if (Neg b)   = IF (bool2if b) (CIF False) (CIF True)"
+"bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)"
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/bool2if.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/bool2if.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "valif (bool2if b) env = value b env";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/boolex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/boolex	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,2 @@
+datatype boolex = Const bool | Var nat
+                | Neg boolex | And boolex boolex
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/end	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+end
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/ifex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/ifex	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/norm
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/norm	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,5 @@
+consts norm :: ifex => ifex
+primrec
+"norm (CIF b)    = CIF b"
+"norm (VIF x)    = VIF x"
+"norm (IF b t e) = normif b (norm t) (norm e)"
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/norm.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/norm.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "valif (norm b) env = valif b env";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/normal
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/normal	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+consts normal :: ifex => bool
+primrec
+"normal(CIF b) = True"
+"normal(VIF x) = True"
+"normal(IF b t e) = (normal t & normal e &
+      (case b of CIF b => True | VIF x => True | IF x y z => False))"
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/normal_norm.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/normal_norm.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "normal(norm b)";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/normal_normif.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/normal_normif.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "!t e. normal(normif b t e) = (normal t & normal e)";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/normif
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/normif	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,5 @@
+consts normif :: ifex => ifex => ifex => ifex
+primrec
+"normif (CIF b)    t e = IF (CIF b) t e"
+"normif (VIF x)    t e = IF (VIF x) t e"
+"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/normif.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/normif.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "!t e. valif (normif b t e) env = valif (IF b t e) env";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/prolog
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/prolog	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Ifexpr = Main +
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/proof.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/proof.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,2 @@
+by(induct_tac "b" 1);
+by(Auto_tac);
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/valif
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/valif	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+consts valif :: ifex => (nat => bool) => bool
+primrec
+"valif (CIF b)    env = b"
+"valif (VIF x)    env = env x"
+"valif (IF b t e) env = (if valif b env then valif t env
+                                        else valif e env)"
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Ifexpr/value
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/value	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+consts value :: boolex => (nat => bool) => bool
+primrec
+"value (Const b) env = b"
+"value (Var x)   env = env x"
+"value (Neg b)   env = (~ value b env)"
+"value (And b c) env = (value b env & value c env)"
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/Ackermann.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Ackermann.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,7 @@
+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 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/Chain.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Chain.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,7 @@
+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 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/ConstDefs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/ConstDefs.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+ConstDefs = Types +
+constdefs nand :: gate
+         "nand A B == ~(A & B)"
+          exor :: gate
+         "exor A B == A & ~B | ~A & B"
+end
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/Defs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Defs.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,5 @@
+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 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/Exor.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Exor.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,5 @@
+Exor = Main +
+constdefs
+ exor :: bool => bool => bool
+"exor A B == (A & ~B) | (~A & B)"
+end
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/Fib.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Fib.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,7 @@
+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 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/GCD.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/GCD.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,14 @@
+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 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/GCD.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/GCD.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+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 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/InfixTree.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/InfixTree.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,4 @@
+Goal "!xs. linInfixList t xs = infixList t @ xs";
+by(induct_tac "t" 1);
+by(Simp_tac 1);
+by(Asm_simp_tac 1);
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/Itrev.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Itrev.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+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 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/Itrev.thy~
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Itrev.thy~	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+Itrev = Main +
+consts itrev :: 'a list => 'a list => 'a list
+primrec itrev list
+"itrev []     ys = ys"
+"itrev (x#xs) ys = itrev xs (x#ys)"
+end
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/Last.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Last.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+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 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/NatSum.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/NatSum.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,3 @@
+Goal "sum n + sum n = n*(Suc n)";
+by(induct_tac "n" 1);
+by(Auto_tac);
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/NatSum.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/NatSum.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+NatSum = Main +
+consts sum :: nat => nat
+primrec
+"sum 0 = 0"
+"sum (Suc n) = Suc n + sum n"
+end
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/ROOT.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,27 @@
+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 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/Sep.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Sep.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,7 @@
+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 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/Sep2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Sep2.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+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 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/Tree.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Tree.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,3 @@
+Tree = Main +
+datatype 'a tree = Tip | Node ('a tree) 'a ('a tree)
+end
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/Types.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Types.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,5 @@
+Types = Main +
+types number       = nat
+      gate         = bool => bool => bool
+      ('a,'b)alist = "('a * 'b)list"
+end
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/autotac.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/autotac.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+by(Auto_tac);
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/constdefs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/constdefs	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,4 @@
+constdefs nand :: gate
+         "nand A B == ~(A & B)"
+          exor :: gate
+         "exor A B == A & ~B | ~A & B"
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/constdefsprolog
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/constdefsprolog	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+ConstDefs = Types +
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/consts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/consts	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+consts nand, exor :: gate
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/defs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/defs	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,2 @@
+defs nand_def "nand A B == ~(A & B)"
+     exor_def "exor A B == A & ~B | ~A & B"
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/defsprolog
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/defsprolog	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Defs = Types +
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/end	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+end
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/exhaust.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/exhaust.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,2 @@
+Goal "(case xs of [] => [] | y#ys => xs) = xs";
+by(exhaust_tac "xs" 1);
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/exorgoal.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/exorgoal.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goalw [exor_def] "exor A (~A)";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/exorproof.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/exorproof.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+by(simp_tac (simpset() addsimps [exor_def]) 1);
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/induct_auto.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/induct_auto.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,2 @@
+by(induct_tac "xs" 1);
+by(Auto_tac);
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/itrev1.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/itrev1.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "itrev xs [] = rev xs";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/itrev2.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/itrev2.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "itrev xs ys = rev xs @ ys";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/itrev3.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/itrev3.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "!ys. itrev xs ys = rev xs @ ys";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/natsum
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/natsum	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,4 @@
+consts sum :: nat => nat
+primrec
+"sum 0 = 0"
+"sum (Suc n) = Suc n + sum n"
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/natsumprolog
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/natsumprolog	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+NatSum = Main +
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/splitif.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/splitif.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+by(split_tac [split_if] 1);
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/splitlist.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/splitlist.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+by(split_tac [list.split] 1);
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/tree
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/tree	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+datatype 'a tree = Tip | Node ('a tree) 'a ('a tree)
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/treeprolog
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/treeprolog	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Tree = Main +
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/types
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/types	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,3 @@
+types number       = nat
+      gate         = bool => bool => bool
+      ('a,'b)alist = "('a * 'b)list"
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/Misc/typesprolog
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/typesprolog	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Types = Main +
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/ToyList/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/ROOT.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+use_thy "ToyList";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/ToyList/ToyList.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/ToyList.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,19 @@
+Goal "xs @ [] = xs";
+by(induct_tac "xs" 1);
+by(Auto_tac);
+qed "app_Nil2";
+Addsimps [app_Nil2];
+Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";
+by(induct_tac "xs" 1);
+by(Auto_tac);
+qed "app_assoc";
+Addsimps [app_assoc];
+Goal "rev(xs @ ys) = (rev ys) @ (rev xs)";
+by(induct_tac "xs" 1);
+by(Auto_tac);
+qed "rev_app";
+Addsimps [rev_app];
+Goal "rev(rev xs) = xs";
+by(induct_tac "xs" 1);
+by(Auto_tac);
+qed "rev_rev";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/ToyList/ToyList.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/ToyList.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,17 @@
+ToyList = Datatype +
+
+datatype 'a list = Nil                        ("[]")
+                 | Cons 'a ('a list)          (infixr "#" 65)
+
+consts app :: 'a list => 'a list => 'a list   (infixr "@" 65)
+       rev :: 'a list => 'a list
+
+primrec
+"[] @ ys       = ys"
+"(x # xs) @ ys = x # (xs @ ys)"
+
+primrec
+"rev []        = []"
+"rev (x # xs)  = (rev xs) @ (x # [])"
+
+end
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/ToyList/addsimps2
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/addsimps2	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Addsimps [app_Nil2];
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/ToyList/autotac
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/autotac	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+by(Auto_tac);
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/ToyList/inductxs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/inductxs	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+by(induct_tac "xs" 1);
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/ToyList/lemma1
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/lemma1	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "rev(xs @ ys) = (rev ys) @ (rev xs)";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/ToyList/lemma2
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/lemma2	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "xs @ [] = xs";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/ToyList/lemma3
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/lemma3	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,3 @@
+Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";
+by(induct_tac "xs" 1);
+by(Auto_tac);
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/ToyList/qed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/qed	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+qed "rev_rev";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/ToyList/qed1
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/qed1	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,2 @@
+qed "rev_app";
+Addsimps [rev_app];
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/ToyList/qed2
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/qed2	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+qed "app_Nil2";
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/ToyList/qed3
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/qed3	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,2 @@
+qed "app_assoc";
+Addsimps [app_assoc];
diff -r 60b31a24f1a6 -r efb799c5ed3c doc-src/Tutorial/ToyList/thm
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/thm	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "rev(rev xs) = xs";