src/HOL/HOLCF/Tutorial/New_Domain.thy
changeset 62175 8ffc4d0e652d
parent 58880 0baae4311a9f
     1.1 --- a/src/HOL/HOLCF/Tutorial/New_Domain.thy	Wed Jan 13 23:02:28 2016 +0100
     1.2 +++ b/src/HOL/HOLCF/Tutorial/New_Domain.thy	Wed Jan 13 23:07:06 2016 +0100
     1.3 @@ -2,57 +2,57 @@
     1.4      Author:     Brian Huffman
     1.5  *)
     1.6  
     1.7 -section {* Definitional domain package *}
     1.8 +section \<open>Definitional domain package\<close>
     1.9  
    1.10  theory New_Domain
    1.11  imports HOLCF
    1.12  begin
    1.13  
    1.14 -text {*
    1.15 +text \<open>
    1.16    UPDATE: The definitional back-end is now the default mode of the domain
    1.17 -  package. This file should be merged with @{text Domain_ex.thy}.
    1.18 -*}
    1.19 +  package. This file should be merged with \<open>Domain_ex.thy\<close>.
    1.20 +\<close>
    1.21  
    1.22 -text {*
    1.23 -  Provided that @{text domain} is the default sort, the @{text new_domain}
    1.24 +text \<open>
    1.25 +  Provided that \<open>domain\<close> is the default sort, the \<open>new_domain\<close>
    1.26    package should work with any type definition supported by the old
    1.27    domain package.
    1.28 -*}
    1.29 +\<close>
    1.30  
    1.31  domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
    1.32  
    1.33 -text {*
    1.34 +text \<open>
    1.35    The difference is that the new domain package is completely
    1.36    definitional, and does not generate any axioms.  The following type
    1.37    and constant definitions are not produced by the old domain package.
    1.38 -*}
    1.39 +\<close>
    1.40  
    1.41  thm type_definition_llist
    1.42  thm llist_abs_def llist_rep_def
    1.43  
    1.44 -text {*
    1.45 +text \<open>
    1.46    The new domain package also adds support for indirect recursion with
    1.47    user-defined datatypes.  This definition of a tree datatype uses
    1.48    indirect recursion through the lazy list type constructor.
    1.49 -*}
    1.50 +\<close>
    1.51  
    1.52  domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
    1.53  
    1.54 -text {*
    1.55 +text \<open>
    1.56    For indirect-recursive definitions, the domain package is not able to
    1.57    generate a high-level induction rule.  (It produces a warning
    1.58    message instead.)  The low-level reach lemma (now proved as a
    1.59    theorem, no longer generated as an axiom) can be used to derive
    1.60    other induction rules.
    1.61 -*}
    1.62 +\<close>
    1.63  
    1.64  thm ltree.reach
    1.65  
    1.66 -text {*
    1.67 +text \<open>
    1.68    The definition of the take function uses map functions associated with
    1.69    each type constructor involved in the definition.  A map function
    1.70    for the lazy list type has been generated by the new domain package.
    1.71 -*}
    1.72 +\<close>
    1.73  
    1.74  thm ltree.take_rews
    1.75  thm llist_map_def