src/HOLCF/ex/loeckx.ML
 changeset 10835 f4745d77e620 parent 9248 e1dee89de037 child 13524 604d0f3622d6
```     1.1 --- a/src/HOLCF/ex/loeckx.ML	Tue Jan 09 15:32:27 2001 +0100
1.2 +++ b/src/HOLCF/ex/loeckx.ML	Tue Jan 09 15:36:30 2001 +0100
1.3 @@ -19,16 +19,16 @@
1.4  Since we already proved the theorem
1.5
1.6  val cont_lubcfun = prove_goal Cfun2.thy
1.7 -        "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))"
1.8 +        "chain ?F ==> cont (%x. lub (range (%j. ?F j\$x)))"
1.9
1.10
1.11  it suffices to prove:
1.12
1.13 -Ifix  = (%f.lub (range (%j. (LAM f. iterate j f UU)`f)))
1.14 +Ifix  = (%f.lub (range (%j. (LAM f. iterate j f UU)\$f)))
1.15
1.16  and
1.17
1.18 -cont (%f.lub (range (%j. (LAM f. iterate j f UU)`f)))
1.19 +cont (%f.lub (range (%j. (LAM f. iterate j f UU)\$f)))
1.20
1.21  Note that if we use the term
1.22
1.23 @@ -40,15 +40,15 @@
1.24
1.25  Goal "cont(Ifix)";
1.26  by (res_inst_tac
1.27 - [("t","Ifix"),("s","(%f. lub(range(%j.(LAM f. iterate j f UU)`f)))")]
1.28 + [("t","Ifix"),("s","(%f. lub(range(%j.(LAM f. iterate j f UU)\$f)))")]
1.29    ssubst 1);
1.30  by (rtac ext 1);
1.31  by (rewtac Ifix_def );
1.32  by (subgoal_tac
1.33 -  "range(% i. iterate i f UU) = range(%j.(LAM f. iterate j f UU)`f)" 1);
1.34 +  "range(% i. iterate i f UU) = range(%j.(LAM f. iterate j f UU)\$f)" 1);
1.35  by (etac arg_cong 1);
1.36  by (subgoal_tac
1.37 -        "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)" 1);
1.38 +        "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)\$f)" 1);
1.39  by (etac arg_cong 1);
1.40  by (rtac ext 1);
1.41  by (stac beta_cfun 1);
1.42 @@ -70,19 +70,19 @@
1.43
1.44  (* the proof in little steps *)
1.45
1.46 -Goal "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)";
1.47 +Goal "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)\$f)";
1.48  by (rtac ext 1);
1.49  by (simp_tac (simpset() addsimps [beta_cfun, cont2cont_CF1L, cont_iterate]) 1);
1.50  qed "fix_lemma1";
1.51
1.52 -Goal "Ifix = (%f. lub(range(%j.(LAM f. iterate j f UU)`f)))";
1.53 +Goal "Ifix = (%f. lub(range(%j.(LAM f. iterate j f UU)\$f)))";
1.54  by (rtac ext 1);
1.55  by (simp_tac (simpset() addsimps [Ifix_def, fix_lemma1]) 1);
1.56  qed "fix_lemma2";
1.57
1.58  (*
1.59  - cont_lubcfun;
1.60 -val it = "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" : thm
1.61 +val it = "chain ?F ==> cont (%x. lub (range (%j. ?F j\$x)))" : thm
1.62
1.63  *)
1.64
```