src/ZF/List_ZF.thy

 (*  Title:      ZF/List_ZF.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 *)
 
-section{*Lists in Zermelo-Fraenkel Set Theory*}
+section\<open>Lists in Zermelo-Fraenkel Set Theory\<close>
 
 theory List_ZF imports Datatype_ZF ArithSimp begin
 
 consts
   list       :: "i=>i"

   "take(n, as) == list_rec(\<lambda>n\<in>nat. [],
                 %a l r. \<lambda>n\<in>nat. nat_case([], %m. Cons(a, r`m), n), as)`n"
 
 definition
   nth :: "[i, i]=>i"  where
-  --{*returns the (n+1)th element of a list, or 0 if the
-   list is too short.*}
+  --\<open>returns the (n+1)th element of a list, or 0 if the
+   list is too short.\<close>
   "nth(n, as) == list_rec(\<lambda>n\<in>nat. 0,
                           %a l r. \<lambda>n\<in>nat. nat_case(a, %m. r`m, n), as) ` n"
 
 definition
   list_update :: "[i, i, i]=>i"  where

      "xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] \<longleftrightarrow> (xs = ys & x=y)"
 apply (erule list.induct)
  apply clarify
  apply (erule list.cases)
  apply simp_all
-txt{*Inductive step*}
+txt\<open>Inductive step\<close>
 apply clarify
 apply (erule_tac a=ys in list.cases, simp_all)
 done
 
 

      "l\<in>list(A) ==> \<forall>n\<in>nat. length(take(n,l)) = min(n, length(l))"
 apply (induct_tac "l", safe, simp_all)
 apply (erule natE, simp_all)
 done
 
-subsection{*The function zip*}
-
-text{*Crafty definition to eliminate a type argument*}
+subsection\<open>The function zip\<close>
+
+text\<open>Crafty definition to eliminate a type argument\<close>
 
 consts
   zip_aux        :: "[i,i]=>i"
 
 primrec (*explicit lambda is required because both arguments of "un" vary*)

      "xs \<in> list(B) ==> sublist(xs, A \<inter> nat) = sublist(xs, A)"
 apply (erule list.induct)
 apply (simp_all add: sublist_Cons)
 done
 
-text{*Repetition of a List Element*}
+text\<open>Repetition of a List Element\<close>
 
 consts   repeat :: "[i,i]=>i"
 primrec
   "repeat(a,0) = []"