src/HOL/Induct/QuoDataType.thy
changeset 15120 f0359f75682e
parent 14658 b1293d0f8d5f
child 15152 5c4d3f10ac5a
     1.1 --- a/src/HOL/Induct/QuoDataType.thy	Fri Aug 06 16:54:26 2004 +0200
     1.2 +++ b/src/HOL/Induct/QuoDataType.thy	Fri Aug 06 16:55:14 2004 +0200
     1.3 @@ -147,15 +147,15 @@
     1.4  
     1.5    MPair :: "[msg,msg] \<Rightarrow> msg"
     1.6     "MPair X Y ==
     1.7 -       Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> \<Union>\<^bsub>V \<in> Rep_Msg Y\<^esub> msgrel``{MPAIR U V})"
     1.8 +       Abs_Msg (\<Union>U \<in> Rep_Msg X. \<Union>V \<in> Rep_Msg Y. msgrel``{MPAIR U V})"
     1.9  
    1.10    Crypt :: "[nat,msg] \<Rightarrow> msg"
    1.11     "Crypt K X ==
    1.12 -       Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> msgrel``{CRYPT K U})"
    1.13 +       Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{CRYPT K U})"
    1.14  
    1.15    Decrypt :: "[nat,msg] \<Rightarrow> msg"
    1.16     "Decrypt K X ==
    1.17 -       Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> msgrel``{DECRYPT K U})"
    1.18 +       Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{DECRYPT K U})"
    1.19  
    1.20  
    1.21  text{*Reduces equality of equivalence classes to the @{term msgrel} relation:
    1.22 @@ -228,7 +228,7 @@
    1.23  
    1.24  constdefs
    1.25    nonces :: "msg \<Rightarrow> nat set"
    1.26 -   "nonces X == \<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> freenonces U"
    1.27 +   "nonces X == \<Union>U \<in> Rep_Msg X. freenonces U"
    1.28  
    1.29  lemma nonces_congruent: "congruent msgrel freenonces"
    1.30  by (simp add: congruent_def msgrel_imp_eq_freenonces) 
    1.31 @@ -263,7 +263,7 @@
    1.32  
    1.33  constdefs
    1.34    left :: "msg \<Rightarrow> msg"
    1.35 -   "left X == Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> msgrel``{freeleft U})"
    1.36 +   "left X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
    1.37  
    1.38  lemma left_congruent: "congruent msgrel (\<lambda>U. msgrel `` {freeleft U})"
    1.39  by (simp add: congruent_def msgrel_imp_eqv_freeleft) 
    1.40 @@ -297,7 +297,7 @@
    1.41  
    1.42  constdefs
    1.43    right :: "msg \<Rightarrow> msg"
    1.44 -   "right X == Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> msgrel``{freeright U})"
    1.45 +   "right X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
    1.46  
    1.47  lemma right_congruent: "congruent msgrel (\<lambda>U. msgrel `` {freeright U})"
    1.48  by (simp add: congruent_def msgrel_imp_eqv_freeright)