diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/ex/LList.thy
--- a/src/ZF/ex/LList.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/LList.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -30,7 +30,7 @@
   standard pairs work just as well.  To use variant pairs, must change prefix
   a q/Q to the Sigma, Pair and converse rules.*)
 coinductive
-  domains "lleq(A)" <= "llist(A) * llist(A)"
+  domains "lleq(A)" \<subseteq> "llist(A) * llist(A)"
   intros
     LNil:  "<LNil, LNil> \<in> lleq(A)"
     LCons: "[| a \<in> A; <l,l'> \<in> lleq(A) |] 
@@ -74,7 +74,7 @@
 inductive_cases LConsE: "LCons(a,l) \<in> llist(A)"
 
 (*Proving freeness results*)
-lemma LCons_iff: "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'"
+lemma LCons_iff: "LCons(a,l)=LCons(a',l') \<longleftrightarrow> a=a' & l=l'"
 by auto
 
 lemma LNil_LCons_iff: "~ LNil=LCons(a,l)"
@@ -107,7 +107,7 @@
 declare Ord_in_Ord [elim!]
 
 lemma llist_quniv_lemma [rule_format]:
-     "Ord(i) ==> \<forall>l \<in> llist(quniv(A)). l Int Vset(i) \<subseteq> univ(eclose(A))"
+     "Ord(i) ==> \<forall>l \<in> llist(quniv(A)). l \<inter> Vset(i) \<subseteq> univ(eclose(A))"
 apply (erule trans_induct)
 apply (rule ballI)
 apply (erule llist.cases)
@@ -135,7 +135,7 @@
 
 (*Lemma for proving finality.  Unfold the lazy list; use induction hypothesis*)
 lemma lleq_Int_Vset_subset [rule_format]:
-     "Ord(i) ==> \<forall>l l'. <l,l'> \<in> lleq(A) --> l Int Vset(i) \<subseteq> l'"
+     "Ord(i) ==> \<forall>l l'. <l,l'> \<in> lleq(A) \<longrightarrow> l \<inter> Vset(i) \<subseteq> l'"
 apply (erule trans_induct)
 apply (intro allI impI)
 apply (erule lleq.cases)
@@ -200,7 +200,7 @@
         flip_LCons [simp] 
         not_type [simp]
 
-lemma bool_Int_subset_univ: "b \<in> bool ==> b Int X \<subseteq> univ(eclose(A))"
+lemma bool_Int_subset_univ: "b \<in> bool ==> b \<inter> X \<subseteq> univ(eclose(A))"
 by (fast intro: Int_lower1 [THEN subset_trans] elim!: boolE)
 
 declare not_type [intro!]
@@ -209,7 +209,7 @@
 (*Reasoning borrowed from lleq.ML; a similar proof works for all
   "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
 lemma flip_llist_quniv_lemma [rule_format]:
-     "Ord(i) ==> \<forall>l \<in> llist(bool). flip(l) Int Vset(i) \<subseteq> univ(eclose(bool))"
+     "Ord(i) ==> \<forall>l \<in> llist(bool). flip(l) \<inter> Vset(i) \<subseteq> univ(eclose(bool))"
 apply (erule trans_induct)
 apply (rule ballI)
 apply (erule llist.cases, simp_all)