# HG changeset patch
# User nipkow
# Date 801151137 -7200
# Node ID 13a3df2adbe52a7be01d8fcd15307be2f1ae744d
# Parent  a6233ea105a466c4dff068dace45950e6d0922ef
Added Park induction to Lfp.
Added Lambda to Makefile.

diff -r a6233ea105a4 -r 13a3df2adbe5 src/HOL/Lfp.ML
--- a/src/HOL/Lfp.ML	Mon May 22 14:12:40 1995 +0200
+++ b/src/HOL/Lfp.ML	Mon May 22 15:58:57 1995 +0200
@@ -37,7 +37,6 @@
 by (REPEAT (resolve_tac [equalityI,lfp_lemma2,lfp_lemma3,mono] 1));
 qed "lfp_Tarski";
 
-
 (*** General induction rule for least fixed points ***)
 
 val [lfp,mono,indhyp] = goal Lfp.thy
@@ -63,6 +62,13 @@
 by(asm_simp_tac (prod_ss addsimps prems) 1);
 qed"induct2";
 
+(*** Fixpoint induction a la David Park ***)
+goal Lfp.thy "!!f. [| mono f; f A <= A |] ==> lfp(f) <= A";
+br subsetI 1;
+by(EVERY[etac induct 1, atac 1, etac subsetD 1, rtac subsetD 1,
+                atac 2, fast_tac (set_cs addSEs [monoD]) 1]);
+qed "Park_induct";
+
 (** Definition forms of lfp_Tarski and induct, to control unfolding **)
 
 val [rew,mono] = goal Lfp.thy "[| h==lfp(f);  mono(f) |] ==> h = f(h)";
diff -r a6233ea105a4 -r 13a3df2adbe5 src/HOL/Makefile
--- a/src/HOL/Makefile	Mon May 22 14:12:40 1995 +0200
+++ b/src/HOL/Makefile	Mon May 22 15:58:57 1995 +0200
@@ -98,6 +98,15 @@
 Subst:  $(BIN)/CHOL  $(SUBST_FILES)
 	echo 'exit_use"Subst/ROOT.ML";quit();' | $(LOGIC)
 
+##Confluence of Lambda-calculus
+LAMBDA_NAMES = Lambda ParRed Confluence
+
+LAMBDA_FILES = Lambda/ROOT.ML \
+              $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
+
+Lambda:  $(BIN)/CHOL  $(LAMBDA_FILES)
+	echo 'exit_use"Lambda/ROOT.ML";quit();' | $(LOGIC)
+
 ##Miscellaneous examples
 EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String 
 
@@ -108,7 +117,7 @@
 	echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
 
 #Full test.
-test:   $(BIN)/CHOL IMP Integ IOA Subst ex
+test:   $(BIN)/CHOL IMP Integ IOA Subst Lambda ex
 	echo 'Test examples ran successfully' > test
 
 .PRECIOUS:  $(BIN)/Pure $(BIN)/CHOL