Prod is now a parent of Lfp.
Added thm induct2 to Lfp.
Changed the way patterns in abstractions are pretty printed.
It has become simpler now but fails if split has more than one argument
because then the ast-translation does not match.

--- a/src/HOL/HOL.thy	Tue May 09 10:43:19 1995 +0200
+++ b/src/HOL/HOL.thy	Tue May 09 22:10:08 1995 +0200
@@ -101,8 +101,7 @@
   "EX xs. P"    => "? xs. P"
   "EX! xs. P"   => "?! xs. P"
   "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
-  "let x = a in e"          == "Let a (%x. e)"
-
+  "let x = a in e"        == "Let a (%x. e)"
 
 rules
 

--- a/src/HOL/Lfp.ML	Tue May 09 10:43:19 1995 +0200
+++ b/src/HOL/Lfp.ML	Tue May 09 22:10:08 1995 +0200
@@ -52,6 +52,17 @@
 	    rtac (CollectI RS subsetI), rtac indhyp, atac]);
 qed "induct";
 
+val major::prems = goal Lfp.thy
+  "[| (a,b) : lfp f; mono f; \
+\     !!a b. (a,b) : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b";
+by(res_inst_tac [("c1","P")] (split RS subst) 1);
+br (major RS induct) 1;
+brs prems 1;
+by(res_inst_tac[("p","x")]PairE 1);
+by(hyp_subst_tac 1);
+by(asm_simp_tac (prod_ss addsimps prems) 1);
+qed"induct2";
+
 (** Definition forms of lfp_Tarski and induct, to control unfolding **)
 
 val [rew,mono] = goal Lfp.thy "[| h==lfp(f);  mono(f) |] ==> h = f(h)";

--- a/src/HOL/Lfp.thy	Tue May 09 10:43:19 1995 +0200
+++ b/src/HOL/Lfp.thy	Tue May 09 22:10:08 1995 +0200
@@ -6,7 +6,7 @@
 The Knaster-Tarski Theorem
 *)
 
-Lfp = mono + 
+Lfp = mono + Prod +
 consts lfp :: "['a set=>'a set] => 'a set"
 defs
  (*least fixed point*)

--- a/src/HOL/Prod.thy	Tue May 09 10:43:19 1995 +0200
+++ b/src/HOL/Prod.thy	Tue May 09 22:10:08 1995 +0200
@@ -40,16 +40,16 @@
 syntax
   "@Tuple"      :: "['a, args] => 'a * 'b"            ("(1'(_,/ _'))")
 
-  "@pttrn"  :: "pttrns => pttrn"            ("'(_')")
-  ""        :: " pttrn           => pttrns" ("_")
-  "@pttrns" :: "[pttrn,pttrns]   => pttrns" ("_,/_")
+  "@pttrn"  :: "[pttrn,pttrns] => pttrn"              ("'(_,/_')")
+  ""        :: " pttrn         => pttrns"             ("_")
+  "@pttrns" :: "[pttrn,pttrns] => pttrns"             ("_,/_")
 
 translations
   "(x, y, z)"   == "(x, (y, z))"
   "(x, y)"      == "Pair x y"
 
-  "%(x,y,zs).b"   => "split(%x (y,zs).b)"
-  "%(x,y).b"      => "split(%x y.b)"
+  "%(x,y,zs).b"   == "split(%x (y,zs).b)"
+  "%(x,y).b"      == "split(%x y.b)"
 (* The <= direction fails if split has more than one argument because
    ast-matching fails. Otherwise it would work fine *)
 
@@ -75,12 +75,12 @@
   Unity_def     "() == Abs_Unit(True)"
 
 end
-
+(*
 ML
 
 local open Syntax
 
-fun pttrn s = const"@pttrn" $ s;
+fun pttrn(_ $ s $ t) = const"@pttrn" $ s $ t;
 fun pttrns s t = const"@pttrns" $ s $ t;
 
 fun split2(Abs(x,T,t)) =
@@ -102,3 +102,4 @@
 val print_translation = [("split", split_tr')];
 
 end;
+*)