# HG changeset patch
# User nipkow
# Date 800050248 -7200
# Node ID c2d51f10b9ee5f0d9a6a88dbbdcf477eb14b4a95
# Parent  c8dfb56a7e95b998b7cbc9a6fedd84370c92c6b8
Moved induct2 from Hoare to Lfp.

diff -r c8dfb56a7e95 -r c2d51f10b9ee src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Tue May 09 22:10:08 1995 +0200
+++ b/src/HOL/IMP/Hoare.ML	Tue May 09 22:10:48 1995 +0200
@@ -38,17 +38,6 @@
 by(fast_tac comp_cs 1);
 qed"hoare_if";
 
-val major::prems = goal Hoare.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";
-
 goalw Hoare.thy (spec_def::C_simps)
   "!!P. [| {{%s. P s & B b s}} c {{P}} |] ==> \
 \  {{P}} while b do c {{%s. P s & ~B b s}}";