# HG changeset patch
# User nipkow
# Date 867314595 -7200
# Node ID 7bf1e7c40a0ca10ccb1ffe7c3e4294814f51d08c
# Parent  5d71eed16fbe66797885434e018a78a7c945b74e
amdI -> admI2

diff -r 5d71eed16fbe -r 7bf1e7c40a0c src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Jun 26 10:42:50 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Jun 26 10:43:15 1997 +0200
@@ -7,20 +7,6 @@
 
 *)
 
-(* FIX: Put into Fix.ML to adm_lemmas !!! *)
-
-goal thy "!! P. [| adm (%x. P x --> Q x); adm (%x.Q x --> P x) |] \
-\           ==> adm (%x. P x = Q x)";
-by (res_inst_tac [("P2","(%x.(P x --> Q x) & (Q x --> P x))")] (adm_cong RS iffD1) 1);
-by (Fast_tac 1);
-by (etac adm_conj 1);
-by (assume_tac 1);
-qed"adm_iff";
-
-Addsimps [adm_iff];
-
-
-
 Addsimps [andalso_and,andalso_or];
 
 (* ----------------------------------------------------------------------------------- *)
@@ -486,7 +472,7 @@
 section "admissibility";
 
 (* Finite x is proven to be adm: Finite_flat shows that there are only chains of length one.
-   Then the assumption that an _infinite_ chain exists (from admI) is set to a contradiction 
+   Then the assumption that an _infinite_ chain exists (from admI2) is set to a contradiction 
    to Finite_flat *)
 
 goal thy "!! (x:: 'a Seq). Finite x ==> !y. Finite (y:: 'a Seq) & x<<y --> x=y";
@@ -502,7 +488,7 @@
 
 
 goal thy "adm(%(x:: 'a Seq).Finite x)";
-by (rtac admI 1);
+by (rtac admI2 1);
 by (eres_inst_tac [("x","0")] allE 1);
 back();
 by (etac exE 1);
diff -r 5d71eed16fbe -r 7bf1e7c40a0c src/HOLCF/ex/Stream.ML
--- a/src/HOLCF/ex/Stream.ML	Thu Jun 26 10:42:50 1997 +0200
+++ b/src/HOLCF/ex/Stream.ML	Thu Jun 26 10:43:15 1997 +0200
@@ -363,7 +363,7 @@
 	fast_tac (HOL_cs addSIs [stream_finite_UU, stream_finite_lemma1]) 1]);
 
 qed_goal "adm_not_stream_finite" thy "adm (%x. ~  stream_finite x)" (fn _ => [
-	rtac admI 1,
+	rtac admI2 1,
 	dtac spec 1,
 	etac contrapos 1,
 	dtac stream_finite_less 1,