src/HOL/Record.thy

     Author:     Norbert Schirmer, TU Muenchen
     Author:     Thomas Sewell, NICTA
     Author:     Florian Haftmann, TU Muenchen
 *)
 
-section {* Extensible records with structural subtyping *}
+section \<open>Extensible records with structural subtyping\<close>
 
 theory Record
 imports Quickcheck_Exhaustive
 keywords "record" :: thy_decl
 begin
 
-subsection {* Introduction *}
-
-text {*
+subsection \<open>Introduction\<close>
+
+text \<open>
   Records are isomorphic to compound tuple types. To implement
   efficient records, we make this isomorphism explicit. Consider the
   record access/update simplification @{text "alpha (beta_update f
   rec) = alpha rec"} for distinct fields alpha and beta of some record
   rec with n fields. There are @{text "n ^ 2"} such theorems, which

   possible pattern matches. The rule set is used as it is viewed
   outside the locale, with the locale assumption (that the isomorphism
   is valid) left as a rule assumption. All rules are structured to aid
   net matching, using either a point-free form or an encapsulating
   predicate.
-*}
-
-subsection {* Operators and lemmas for types isomorphic to tuples *}
+\<close>
+
+subsection \<open>Operators and lemmas for types isomorphic to tuples\<close>
 
 datatype (dead 'a, dead 'b, dead 'c) tuple_isomorphism =
   Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
 
 primrec

   iso_tuple_cons ::
     "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where
   "iso_tuple_cons isom = curry (abst isom)"
 
 
-subsection {* Logical infrastructure for records *}
+subsection \<open>Logical infrastructure for records\<close>
 
 definition
   iso_tuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
   "iso_tuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y"
 

 
 lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)"
   by (simp add: comp_def)
 
 
-subsection {* Concrete record syntax *}
+subsection \<open>Concrete record syntax\<close>
 
 nonterminal
   ident and
   field_type and
   field_types and

   "_record"             :: "fields => 'a"                       ("(3\<lparr>_\<rparr>)")
   "_record_scheme"      :: "fields => 'a => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   "_record_update"      :: "'a => field_updates => 'b"          ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
 
 
-subsection {* Record package *}
+subsection \<open>Record package\<close>
 
 ML_file "Tools/record.ML"
 
 hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
   iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons