# HG changeset patch # User berghofe # Date 1210150793 -7200 # Node ID 7f7c6a9e083a48cb1b0efa63bbced23dee94c061 # Parent 535290c908ae28895f5b69caa30868e58113fc70 Instantiated rule increasing_chain_adm_lemma in proof of flatstream_adm_lemma to avoid problems with HO unification. diff -r 535290c908ae -r 7f7c6a9e083a src/HOLCF/FOCUS/Stream_adm.thy --- a/src/HOLCF/FOCUS/Stream_adm.thy Wed May 07 10:59:52 2008 +0200 +++ b/src/HOLCF/FOCUS/Stream_adm.thy Wed May 07 10:59:53 2008 +0200 @@ -36,7 +36,7 @@ assumes 3: "(!!Y. [| Porder.chain Y; !i. P (Y i); !k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(lub (range Y)))" shows "P(lub (range Y))" -apply (rule increasing_chain_adm_lemma [OF 1 2]) +apply (rule increasing_chain_adm_lemma [of _ P, OF 1 2]) apply (erule 3, assumption) apply (erule thin_rl) apply (rule allI)