Nominal/Nominal2_Abs.thy
changeset 2592 98236fbd8aa6
parent 2591 35c570891a3a
child 2599 d6fe94028a5d
equal deleted inserted replaced
2591:35c570891a3a 2592:98236fbd8aa6
   253 quotient_type 
   253 quotient_type 
   254     'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set"
   254     'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set"
   255 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
   255 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
   256 and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst"
   256 and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst"
   257   apply(rule_tac [!] equivpI)
   257   apply(rule_tac [!] equivpI)
   258   unfolding reflp_def symp_def transp_def
   258   unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def
   259   by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
   259   by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
   260 
   260 
   261 quotient_definition
   261 quotient_definition
   262   Abs_set ("[_]set. _" [60, 60] 60)
   262   Abs_set ("[_]set. _" [60, 60] 60)
   263 where
   263 where