# HG changeset patch
# User oheimb
# Date 854725167 -3600
# Node ID f86367e104f5a16b32219c4cad7c1a30a436c1b6
# Parent  7a28e02e10b7014ecb9c2bc7fdf282b2ac3122ae
added def_fix_ind and def_wfix_ind for convenience

diff -r 7a28e02e10b7 -r f86367e104f5 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Fri Jan 31 15:54:00 1997 +0100
+++ b/src/HOLCF/Fix.ML	Fri Jan 31 16:39:27 1997 +0100
@@ -499,6 +499,14 @@
         (atac 1)
         ]);
 
+qed_goal "def_fix_ind" Fix.thy "[| f == fix`F; adm(P); \
+\       P(UU);!!x. P(x) ==> P(F`x)|] ==> P f" (fn prems => [
+        (cut_facts_tac prems 1),
+	(asm_simp_tac HOL_ss 1),
+	(etac fix_ind 1),
+	(atac 1),
+	(eresolve_tac prems 1)]);
+	
 (* ------------------------------------------------------------------------ *)
 (* computational induction for weak admissible formulae                     *)
 (* ------------------------------------------------------------------------ *)
@@ -515,6 +523,13 @@
         (etac spec 1)
         ]);
 
+qed_goal "def_wfix_ind" Fix.thy "[| f == fix`F; admw(P); \
+\       !n. P(iterate n F UU) |] ==> P f" (fn prems => [
+        (cut_facts_tac prems 1),
+	(asm_simp_tac HOL_ss 1),
+	(etac wfix_ind 1),
+	(atac 1)]);
+
 (* ------------------------------------------------------------------------ *)
 (* for chain-finite (easy) types every formula is admissible                *)
 (* ------------------------------------------------------------------------ *)