avoid potential conflict with Eisbach keyword (although keywords are local to the theory context);
authorwenzelm
Thu Apr 30 17:00:50 2015 +0200 (2015-04-30)
changeset 60208d72795f401c3
parent 60207 81a0900f0ddc
child 60209 022ca2799c73
avoid potential conflict with Eisbach keyword (although keywords are local to the theory context);
src/ZF/AC/AC16_WO4.thy
     1.1 --- a/src/ZF/AC/AC16_WO4.thy	Tue Apr 28 13:30:28 2015 +0200
     1.2 +++ b/src/ZF/AC/AC16_WO4.thy	Thu Apr 30 17:00:50 2015 +0200
     1.3 @@ -541,7 +541,7 @@
     1.4                                    THEN apply_type])+
     1.5  done
     1.6  
     1.7 -lemma (in AC16) conclusion:
     1.8 +lemma (in AC16) "conclusion":
     1.9       "\<exists>a f. Ord(a) & domain(f) = a & (\<Union>b<a. f ` b) = x & (\<forall>b<a. f ` b \<lesssim> m)"
    1.10  apply (rule well_ord_LL [THEN exE])
    1.11  apply (rename_tac S)