--- a/src/HOL/Induct/ABexp.ML Sat Feb 03 15:22:57 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(* Title: HOL/Induct/ABexp.ML
- ID: $Id$
- Author: Stefan Berghofer, TU Muenchen
- Copyright 1998 TU Muenchen
-
-Arithmetic and boolean expressions
-*)
-
-(** substitution theorems for arithmetic and boolean expressions **)
-
-(* One variable *)
-Goal
- "evala env (substa (Var(v := a')) a) = evala (env(v := evala env a')) a & \
- \ evalb env (substb (Var(v := a')) b) = evalb (env(v := evala env a')) b";
-by (induct_tac "a b" 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "subst1_aexp_bexp";
-
-(* All variables *)
-Goal
- "evala env (substa s a) = evala (%x. evala env (s x)) a & \
- \ evalb env (substb s b) = evalb (%x. evala env (s x)) b";
-by (induct_tac "a b" 1);
-by (Auto_tac);
-qed "subst_all_aexp_bexp";
--- a/src/HOL/Induct/ABexp.thy Sat Feb 03 15:22:57 2001 +0100
+++ b/src/HOL/Induct/ABexp.thy Sat Feb 03 17:40:16 2001 +0100
@@ -2,52 +2,50 @@
ID: $Id$
Author: Stefan Berghofer, TU Muenchen
Copyright 1998 TU Muenchen
-
-Arithmetic and boolean expressions
*)
-ABexp = Main +
+header {* Arithmetic and boolean expressions *}
+
+theory ABexp = Main:
-datatype
- 'a aexp = IF ('a bexp) ('a aexp) ('a aexp)
- | Sum ('a aexp) ('a aexp)
- | Diff ('a aexp) ('a aexp)
- | Var 'a
- | Num nat
-and
- 'a bexp = Less ('a aexp) ('a aexp)
- | And ('a bexp) ('a bexp)
- | Neg ('a bexp)
+datatype 'a aexp =
+ IF "'a bexp" "'a aexp" "'a aexp"
+ | Sum "'a aexp" "'a aexp"
+ | Diff "'a aexp" "'a aexp"
+ | Var 'a
+ | Num nat
+and 'a bexp =
+ Less "'a aexp" "'a aexp"
+ | And "'a bexp" "'a bexp"
+ | Neg "'a bexp"
-(** evaluation of arithmetic and boolean expressions **)
+text {* \medskip Evaluation of arithmetic and boolean expressions *}
consts
- evala :: ('a => nat) => 'a aexp => nat
- evalb :: ('a => nat) => 'a bexp => bool
+ evala :: "('a => nat) => 'a aexp => nat"
+ evalb :: "('a => nat) => 'a bexp => bool"
primrec
- "evala env (IF b a1 a2) =
- (if evalb env b then evala env a1 else evala env a2)"
+ "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
"evala env (Sum a1 a2) = evala env a1 + evala env a2"
"evala env (Diff a1 a2) = evala env a1 - evala env a2"
"evala env (Var v) = env v"
"evala env (Num n) = n"
"evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
- "evalb env (And b1 b2) = (evalb env b1 & evalb env b2)"
- "evalb env (Neg b) = (~ evalb env b)"
+ "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
+ "evalb env (Neg b) = (\<not> evalb env b)"
-(** substitution on arithmetic and boolean expressions **)
+text {* \medskip Substitution on arithmetic and boolean expressions *}
consts
- substa :: ('a => 'b aexp) => 'a aexp => 'b aexp
- substb :: ('a => 'b aexp) => 'a bexp => 'b bexp
+ substa :: "('a => 'b aexp) => 'a aexp => 'b aexp"
+ substb :: "('a => 'b aexp) => 'a bexp => 'b bexp"
primrec
- "substa f (IF b a1 a2) =
- IF (substb f b) (substa f a1) (substa f a2)"
+ "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
"substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
"substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
"substa f (Var v) = f v"
@@ -57,4 +55,20 @@
"substb f (And b1 b2) = And (substb f b1) (substb f b2)"
"substb f (Neg b) = Neg (substb f b)"
+lemma subst1_aexp_bexp:
+ "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a \<and>
+ evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
+ -- {* one variable *}
+ apply (induct a and b)
+ apply simp_all
+ done
+
+lemma subst_all_aexp_bexp:
+ "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a \<and>
+ evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
+ -- {* all variables *}
+ apply (induct a and b)
+ apply auto
+ done
+
end
--- a/src/HOL/Induct/Mutil.ML Sat Feb 03 15:22:57 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,117 +0,0 @@
-(* Title: HOL/Induct/Mutil
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-The Mutilated Chess Board Problem, formalized inductively
-*)
-
-Addsimps (tiling.intrs @ domino.intrs);
-AddIs tiling.intrs;
-
-(** The union of two disjoint tilings is a tiling **)
-
-Goal "t: tiling A ==> u: tiling A --> t Int u = {} --> t Un u : tiling A";
-by (etac tiling.induct 1);
-by (simp_tac (simpset() addsimps [Un_assoc]) 2);
-by Auto_tac;
-qed_spec_mp "tiling_UnI";
-
-AddIs [tiling_UnI];
-
-(*** Chess boards ***)
-
-Goalw [lessThan_def]
- "lessThan(Suc n) <*> B = ({n} <*> B) Un ((lessThan n) <*> B)";
-by Auto_tac;
-qed "Sigma_Suc1";
-
-Goalw [lessThan_def]
- "A <*> lessThan(Suc n) = (A <*> {n}) Un (A <*> (lessThan n))";
-by Auto_tac;
-qed "Sigma_Suc2";
-
-Addsimps [Sigma_Suc1, Sigma_Suc2];
-
-Goal "({i} <*> {n}) Un ({i} <*> {m}) = {(i,m), (i,n)}";
-by Auto_tac;
-qed "sing_Times_lemma";
-
-Goal "{i} <*> lessThan(#2*n) : tiling domino";
-by (induct_tac "n" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_assoc RS sym])));
-by (rtac tiling.Un 1);
-by (auto_tac (claset(), simpset() addsimps [sing_Times_lemma]));
-qed "dominoes_tile_row";
-
-AddSIs [dominoes_tile_row];
-
-Goal "(lessThan m) <*> lessThan(#2*n) : tiling domino";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "dominoes_tile_matrix";
-
-
-(*** "coloured" and Dominoes ***)
-
-Goalw [coloured_def]
- "coloured b Int (insert (i,j) t) = \
-\ (if (i+j) mod #2 = b then insert (i,j) (coloured b Int t) \
-\ else coloured b Int t)";
-by Auto_tac;
-qed "coloured_insert";
-Addsimps [coloured_insert];
-
-Goal "d:domino ==> (EX i j. coloured 0 Int d = {(i,j)}) & \
-\ (EX m n. coloured 1 Int d = {(m,n)})";
-by (etac domino.elim 1);
-by (auto_tac (claset(), simpset() addsimps [mod_Suc]));
-qed "domino_singletons";
-
-Goal "d:domino ==> finite d";
-by (etac domino.elim 1);
-by Auto_tac;
-qed "domino_finite";
-Addsimps [domino_finite];
-
-
-(*** Tilings of dominoes ***)
-
-Goal "t:tiling domino ==> finite t";
-by (etac tiling.induct 1);
-by Auto_tac;
-qed "tiling_domino_finite";
-
-Addsimps [tiling_domino_finite, Int_Un_distrib, Diff_Int_distrib];
-
-Goal "t: tiling domino ==> card(coloured 0 Int t) = card(coloured 1 Int t)";
-by (etac tiling.induct 1);
-by (dtac domino_singletons 2);
-by Auto_tac;
-(*this lemma tells us that both "inserts" are non-trivial*)
-by (subgoal_tac "ALL p C. C Int a = {p} --> p ~: t" 1);
-by (Asm_simp_tac 1);
-by (Blast_tac 1);
-qed "tiling_domino_0_1";
-
-(*Final argument is surprisingly complex*)
-Goal "[| t : tiling domino; \
-\ (i+j) mod #2 = 0; (m+n) mod #2 = 0; \
-\ {(i,j),(m,n)} <= t |] \
-\ ==> (t - {(i,j)} - {(m,n)}) ~: tiling domino";
-by (rtac notI 1);
-by (subgoal_tac "card (coloured 0 Int (t - {(i,j)} - {(m,n)})) < \
-\ card (coloured 1 Int (t - {(i,j)} - {(m,n)}))" 1);
-by (force_tac (claset(), HOL_ss addsimps [tiling_domino_0_1]) 1);
-by (asm_simp_tac (simpset() addsimps [tiling_domino_0_1 RS sym]) 1);
-by (asm_full_simp_tac (simpset() addsimps [coloured_def, card_Diff2_less]) 1);
-qed "gen_mutil_not_tiling";
-
-(*Apply the general theorem to the well-known case*)
-Goal "t = lessThan(#2 * Suc m) <*> lessThan(#2 * Suc n) \
-\ ==> t - {(0,0)} - {(Suc(#2*m), Suc(#2*n))} ~: tiling domino";
-by (rtac gen_mutil_not_tiling 1);
-by (blast_tac (claset() addSIs [dominoes_tile_matrix]) 1);
-by Auto_tac;
-qed "mutil_not_tiling";
-
--- a/src/HOL/Induct/Mutil.thy Sat Feb 03 15:22:57 2001 +0100
+++ b/src/HOL/Induct/Mutil.thy Sat Feb 03 17:40:16 2001 +0100
@@ -1,29 +1,150 @@
-(* Title: HOL/Induct/Mutil
+(* Title: HOL/Induct/Mutil.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
-
-The Mutilated Chess Board Problem, formalized inductively
- Originator is Max Black, according to J A Robinson.
- Popularized as the Mutilated Checkerboard Problem by J McCarthy
*)
-Mutil = Main +
+header {* The Mutilated Chess Board Problem *}
+
+theory Mutil = Main:
-consts tiling :: "'a set set => 'a set set"
+text {*
+ The Mutilated Chess Board Problem, formalized inductively.
+
+ Originator is Max Black, according to J A Robinson. Popularized as
+ the Mutilated Checkerboard Problem by J McCarthy.
+*}
+
+consts tiling :: "'a set set => 'a set set"
inductive "tiling A"
- intrs
- empty "{} : tiling A"
- Un "[| a: A; t: tiling A; a Int t = {} |] ==> a Un t : tiling A"
+ intros [simp, intro]
+ empty: "{} \<in> tiling A"
+ Un: "a \<in> A ==> t \<in> tiling A ==> a \<inter> t = {} ==> a \<union> t \<in> tiling A"
-consts domino :: "(nat*nat)set set"
+consts domino :: "(nat \<times> nat) set set"
inductive domino
- intrs
- horiz "{(i, j), (i, Suc j)} : domino"
- vertl "{(i, j), (Suc i, j)} : domino"
+ intros [simp]
+ horiz: "{(i, j), (i, Suc j)} \<in> domino"
+ vertl: "{(i, j), (Suc i, j)} \<in> domino"
constdefs
- coloured :: "nat => (nat*nat)set"
- "coloured b == {(i,j). (i+j) mod #2 = b}"
+ coloured :: "nat => (nat \<times> nat) set"
+ "coloured b == {(i, j). (i + j) mod #2 = b}"
+
+
+text {* \medskip The union of two disjoint tilings is a tiling *}
+
+lemma tiling_UnI [rule_format, intro]:
+ "t \<in> tiling A ==> u \<in> tiling A --> t \<inter> u = {} --> t \<union> u \<in> tiling A"
+ apply (erule tiling.induct)
+ prefer 2
+ apply (simp add: Un_assoc)
+ apply auto
+ done
+
+
+text {* \medskip Chess boards *}
+
+lemma Sigma_Suc1 [simp]:
+ "lessThan (Suc n) \<times> B = ({n} \<times> B) \<union> ((lessThan n) \<times> B)"
+ apply (unfold lessThan_def)
+ apply auto
+ done
+
+lemma Sigma_Suc2 [simp]:
+ "A \<times> lessThan (Suc n) = (A \<times> {n}) \<union> (A \<times> (lessThan n))"
+ apply (unfold lessThan_def)
+ apply auto
+ done
+
+lemma sing_Times_lemma: "({i} \<times> {n}) \<union> ({i} \<times> {m}) = {(i, m), (i, n)}"
+ apply auto
+ done
+
+lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (#2 * n) \<in> tiling domino"
+ apply (induct n)
+ apply (simp_all add: Un_assoc [symmetric])
+ apply (rule tiling.Un)
+ apply (auto simp add: sing_Times_lemma)
+ done
+
+lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (#2 * n) \<in> tiling domino"
+ apply (induct m)
+ apply auto
+ done
+
+
+text {* \medskip @{term coloured} and Dominoes *}
+
+lemma coloured_insert [simp]:
+ "coloured b \<inter> (insert (i, j) t) =
+ (if (i + j) mod #2 = b then insert (i, j) (coloured b \<inter> t)
+ else coloured b \<inter> t)"
+ apply (unfold coloured_def)
+ apply auto
+ done
+
+lemma domino_singletons:
+ "d \<in> domino ==>
+ (\<exists>i j. coloured 0 \<inter> d = {(i, j)}) \<and>
+ (\<exists>m n. coloured 1 \<inter> d = {(m, n)})"
+ apply (erule domino.cases)
+ apply (auto simp add: mod_Suc)
+ done
+
+lemma domino_finite [simp]: "d \<in> domino ==> finite d"
+ apply (erule domino.cases)
+ apply auto
+ done
+
+
+text {* \medskip Tilings of dominoes *}
+
+lemma tiling_domino_finite [simp]: "t \<in> tiling domino ==> finite t"
+ apply (erule tiling.induct)
+ apply auto
+ done
+
+declare
+ Int_Un_distrib [simp]
+ Diff_Int_distrib [simp]
+
+lemma tiling_domino_0_1:
+ "t \<in> tiling domino ==> card (coloured 0 \<inter> t) = card (coloured 1 \<inter> t)"
+ apply (erule tiling.induct)
+ apply (drule_tac [2] domino_singletons)
+ apply auto
+ apply (subgoal_tac "\<forall>p C. C \<inter> a = {p} --> p \<notin> t")
+ -- {* this lemma tells us that both ``inserts'' are non-trivial *}
+ apply (simp (no_asm_simp))
+ apply blast
+ done
+
+
+text {* \medskip Final argument is surprisingly complex *}
+
+theorem gen_mutil_not_tiling:
+ "t \<in> tiling domino ==>
+ (i + j) mod #2 = 0 ==> (m + n) mod #2 = 0 ==>
+ {(i, j), (m, n)} \<subseteq> t
+ ==> (t - {(i, j)} - {(m, n)}) \<notin> tiling domino"
+ apply (rule notI)
+ apply (subgoal_tac
+ "card (coloured 0 \<inter> (t - {(i, j)} - {(m, n)})) <
+ card (coloured 1 \<inter> (t - {(i, j)} - {(m, n)}))")
+ apply (force simp only: tiling_domino_0_1)
+ apply (simp add: tiling_domino_0_1 [symmetric])
+ apply (simp add: coloured_def card_Diff2_less)
+ done
+
+text {* Apply the general theorem to the well-known case *}
+
+theorem mutil_not_tiling:
+ "t = lessThan (#2 * Suc m) \<times> lessThan (#2 * Suc n)
+ ==> t - {(0, 0)} - {(Suc (#2 * m), Suc (#2 * n))} \<notin> tiling domino"
+ apply (rule gen_mutil_not_tiling)
+ apply (blast intro!: dominoes_tile_matrix)
+ apply auto
+ done
end
--- a/src/HOL/Induct/ROOT.ML Sat Feb 03 15:22:57 2001 +0100
+++ b/src/HOL/Induct/ROOT.ML Sat Feb 03 17:40:16 2001 +0100
@@ -1,16 +1,12 @@
-(* Title: HOL/Induct/ROOT.ML
-Examples of Inductive and Coinductive Definitions.
-*)
-
+time_use_thy "Mutil";
+time_use_thy "Term";
+time_use_thy "ABexp";
+time_use_thy "Tree";
time_use_thy "Sigma_Algebra";
time_use_thy "Perm";
time_use_thy "Comb";
-time_use_thy "Mutil";
time_use_thy "PropLog";
time_use_thy "SList";
time_use_thy "LFilter";
-time_use_thy "Term";
-time_use_thy "ABexp";
time_use_thy "Exp";
-time_use_thy "Tree";
--- a/src/HOL/Induct/Sigma_Algebra.thy Sat Feb 03 15:22:57 2001 +0100
+++ b/src/HOL/Induct/Sigma_Algebra.thy Sat Feb 03 17:40:16 2001 +0100
@@ -4,6 +4,8 @@
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
+header {* Sigma algebras *}
+
theory Sigma_Algebra = Main:
text {*
--- a/src/HOL/Induct/Term.ML Sat Feb 03 15:22:57 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(* Title: HOL/Induct/Term.ML
- ID: $Id$
- Author: Stefan Berghofer, TU Muenchen
- Copyright 1998 TU Muenchen
-
-Terms over a given alphabet -- function applications
-*)
-
-(** a simple theorem about composition of substitutions **)
-
-Goal "(subst_term ((subst_term f1) o f2) t) = \
- \ (subst_term f1 (subst_term f2 t)) & \
- \ (subst_term_list ((subst_term f1) o f2) ts) = \
- \ (subst_term_list f1 (subst_term_list f2 ts))";
-by (induct_tac "t ts" 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "subst_comp";
-
-(**** alternative induction rule ****)
-
-bind_thm ("term_induct2", prove_goal thy
- "[| !!v. P (Var v); \
- \ !!f ts. list_all P ts ==> P (App f ts) |] ==> \
- \ P t & list_all P ts"
- (fn prems =>
- [induct_tac "t ts" 1,
- resolve_tac prems 1,
- resolve_tac prems 1,
- atac 1,
- ALLGOALS Asm_simp_tac]) RS conjunct1);
--- a/src/HOL/Induct/Term.thy Sat Feb 03 15:22:57 2001 +0100
+++ b/src/HOL/Induct/Term.thy Sat Feb 03 17:40:16 2001 +0100
@@ -2,23 +2,23 @@
ID: $Id$
Author: Stefan Berghofer, TU Muenchen
Copyright 1998 TU Muenchen
-
-Terms over a given alphabet -- function applications
*)
-Term = Main +
+header {* Terms over a given alphabet *}
+
+theory Term = Main:
-datatype
- ('a, 'b) term = Var 'a
- | App 'b ((('a, 'b) term) list)
+datatype ('a, 'b) "term" =
+ Var 'a
+ | App 'b "('a, 'b) term list"
-(** substitution function on terms **)
+text {* \medskip Substitution function on terms *}
consts
- subst_term :: "['a => ('a, 'b) term, ('a, 'b) term] => ('a, 'b) term"
+ subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
subst_term_list ::
- "['a => ('a, 'b) term, ('a, 'b) term list] => ('a, 'b) term list"
+ "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
primrec
"subst_term f (Var a) = f a"
@@ -28,4 +28,35 @@
"subst_term_list f (t # ts) =
subst_term f t # subst_term_list f ts"
+
+text {* \medskip A simple theorem about composition of substitutions *}
+
+lemma subst_comp:
+ "(subst_term ((subst_term f1) \<circ> f2) t) =
+ (subst_term f1 (subst_term f2 t)) \<and>
+ (subst_term_list ((subst_term f1) \<circ> f2) ts) =
+ (subst_term_list f1 (subst_term_list f2 ts))"
+ apply (induct t and ts rule: term.induct)
+ apply simp_all
+ done
+
+
+text {* \medskip Alternative induction rule *}
+
+lemma term_induct2:
+ "(!!v. P (Var v)) ==>
+ (!!f ts. list_all P ts ==> P (App f ts))
+ ==> P t"
+proof -
+ case antecedent
+ have "P t \<and> list_all P ts"
+ apply (induct t and ts rule: term.induct)
+ apply (rule antecedent)
+ apply (rule antecedent)
+ apply assumption
+ apply simp_all
+ done
+ thus ?thesis ..
+qed
+
end
--- a/src/HOL/Induct/Tree.ML Sat Feb 03 15:22:57 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(* Title: HOL/Induct/Tree.ML
- ID: $Id$
- Author: Stefan Berghofer, TU Muenchen
- Copyright 1999 TU Muenchen
-
-Infinitely branching trees
-*)
-
-Goal "map_tree g (map_tree f t) = map_tree (g o f) t";
-by (induct_tac "t" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "tree_map_compose";
-
-val prems = Goal "(!!x. P x ==> Q (f x)) ==> \
- \ exists_tree P ts --> exists_tree Q (map_tree f ts)";
-by (induct_tac "ts" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
-by (Fast_tac 1);
-qed "exists_map";
-
--- a/src/HOL/Induct/Tree.thy Sat Feb 03 15:22:57 2001 +0100
+++ b/src/HOL/Induct/Tree.thy Sat Feb 03 17:40:16 2001 +0100
@@ -2,26 +2,39 @@
ID: $Id$
Author: Stefan Berghofer, TU Muenchen
Copyright 1999 TU Muenchen
-
-Infinitely branching trees
*)
-Tree = Main +
+header {* Infinitely branching trees *}
+
+theory Tree = Main:
-datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
+datatype 'a tree =
+ Atom 'a
+ | Branch "nat => 'a tree"
consts
map_tree :: "('a => 'b) => 'a tree => 'b tree"
-
primrec
"map_tree f (Atom a) = Atom (f a)"
- "map_tree f (Branch ts) = Branch (%x. map_tree f (ts x))"
+ "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
+
+lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
+ apply (induct t)
+ apply simp_all
+ done
consts
exists_tree :: "('a => bool) => 'a tree => bool"
-
primrec
"exists_tree P (Atom a) = P a"
- "exists_tree P (Branch ts) = (? x. exists_tree P (ts x))"
+ "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
+
+lemma exists_map:
+ "(!!x. P x ==> Q (f x)) ==>
+ exists_tree P ts ==> exists_tree Q (map_tree f ts)"
+ apply (induct ts)
+ apply simp_all
+ apply blast
+ done
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/document/root.tex Sat Feb 03 17:40:16 2001 +0100
@@ -0,0 +1,27 @@
+
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym,pdfsetup}
+
+%for best-style documents ...
+\urlstyle{rm}
+\isabellestyle{it}
+
+\begin{document}
+
+\title{Examples of Inductive and Coinductive Definitions}
+\author{Stefan Berghofer \\ Tobias Nipkow \\ Lawrence C Paulson \\ Markus Wenzel}
+\maketitle
+
+\begin{abstract}
+ This is a collection of small examples to demonstrate Isabelle/HOL's
+ (co)inductive definitions package. Large examples appear on many other
+ sessions, such as Lambda, IMP, and Auth.
+\end{abstract}
+
+\tableofcontents
+\newpage
+
+\parindent 0pt\parskip 0.5ex
+\input{session}
+
+\end{document}
--- a/src/HOL/IsaMakefile Sat Feb 03 15:22:57 2001 +0100
+++ b/src/HOL/IsaMakefile Sat Feb 03 17:40:16 2001 +0100
@@ -205,11 +205,11 @@
$(LOG)/HOL-Induct.gz: $(OUT)/HOL \
Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
- Induct/LList.ML Induct/LList.thy Induct/Mutil.ML Induct/Mutil.thy \
- Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML \
- Induct/PropLog.thy Induct/ROOT.ML Induct/Sexp.ML Induct/Sexp.thy \
- Induct/Sigma_Algebra.thy Induct/SList.ML Induct/SList.thy \
- Induct/ABexp.ML Induct/ABexp.thy Induct/Term.ML Induct/Term.thy
+ Induct/LList.ML Induct/LList.thy Induct/Mutil.thy Induct/Perm.ML \
+ Induct/Perm.thy Induct/PropLog.ML Induct/PropLog.thy Induct/ROOT.ML \
+ Induct/Sexp.ML Induct/Sexp.thy Induct/Sigma_Algebra.thy \
+ Induct/SList.ML Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \
+ Induct/Tree.thy Induct/document/root.tex
@$(ISATOOL) usedir $(OUT)/HOL Induct