changed to use new contlubI, etc.
authorhuffman
Fri Jun 03 23:34:49 2005 +0200 (2005-06-03)
changeset 162157ff978ca1920
parent 16214 e3816a7db016
child 16216 279ab2e02089
changed to use new contlubI, etc.
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Up.thy	Fri Jun 03 23:33:48 2005 +0200
     1.2 +++ b/src/HOLCF/Up.thy	Fri Jun 03 23:34:49 2005 +0200
     1.3 @@ -157,10 +157,10 @@
     1.4  subsection {* Monotonicity of @{term Iup} and @{term Ifup} *}
     1.5  
     1.6  lemma monofun_Iup: "monofun(Iup)"
     1.7 -by (simp add: monofun)
     1.8 +by (simp add: monofun_def)
     1.9  
    1.10  lemma monofun_Ifup1: "monofun(Ifup)"
    1.11 -apply (rule monofunI [rule_format])
    1.12 +apply (rule monofunI)
    1.13  apply (rule less_fun [THEN iffD2, rule_format])
    1.14  apply (rule_tac p = "xa" in upE)
    1.15  apply simp
    1.16 @@ -169,7 +169,7 @@
    1.17  done
    1.18  
    1.19  lemma monofun_Ifup2: "monofun(Ifup(f))"
    1.20 -apply (rule monofunI [rule_format])
    1.21 +apply (rule monofunI)
    1.22  apply (rule_tac p = "x" in upE)
    1.23  apply simp
    1.24  apply simp
    1.25 @@ -376,7 +376,7 @@
    1.26  text {* continuity for @{term Iup} *}
    1.27  
    1.28  lemma cont_Iup [iff]: "cont(Iup)"
    1.29 -apply (rule contI [rule_format])
    1.30 +apply (rule contI)
    1.31  apply (rule is_lub_Iup)
    1.32  apply (erule thelubE [OF _ refl])
    1.33  done
    1.34 @@ -386,7 +386,7 @@
    1.35  text {* continuity for @{term Ifup} *}
    1.36  
    1.37  lemma contlub_Ifup1: "contlub(Ifup)"
    1.38 -apply (rule contlubI [rule_format])
    1.39 +apply (rule contlubI)
    1.40  apply (rule trans)
    1.41  apply (rule_tac [2] thelub_fun [symmetric])
    1.42  apply (erule_tac [2] monofun_Ifup1 [THEN ch2ch_monofun])
    1.43 @@ -399,7 +399,7 @@
    1.44  done
    1.45  
    1.46  lemma contlub_Ifup2: "contlub(Ifup(f))"
    1.47 -apply (rule contlubI [rule_format])
    1.48 +apply (rule contlubI)
    1.49  apply (case_tac "EX i x. Y i = Iup x")
    1.50  apply (erule exE)
    1.51  apply (subst thelub_up1c)