src/HOL/HOLCF/Universal.thy

 section \<open>A universal bifinite domain\<close>
 
 theory Universal
 imports Bifinite Completion "~~/src/HOL/Library/Nat_Bijection"
 begin
+
+no_notation binomial  (infixl "choose" 65)
 
 subsection \<open>Basis for universal domain\<close>
 
 subsubsection \<open>Basis datatype\<close>
 

 apply (rule_tac i=a in below_lub)
 apply simp
 apply (simp add: udom_approx_principal)
 apply (simp add: ubasis_until_same ubasis_le_refl)
 done
- 
+
 lemma udom_approx [simp]: "approx_chain udom_approx"
 proof
   show "chain (\<lambda>i. udom_approx i)"
     by (rule chain_udom_approx)
   show "(\<Squnion>i. udom_approx i) = ID"

 instance udom :: bifinite
   by standard (fast intro: udom_approx)
 
 hide_const (open) node
 
+notation binomial  (infixl "choose" 65)
+
 end