1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Sat Mar 13 14:44:47 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Sat Mar 13 15:12:17 2010 +0100
     1.3 @@ -4,17 +4,14 @@
     1.4  
     1.5  chapter {* Isabelle/HOL \label{ch:hol} *}
     1.6  
     1.7 -section {* Primitive types \label{sec:hol-typedef} *}
     1.8 +section {* Typedef axiomatization \label{sec:hol-typedef} *}
     1.9  
    1.10  text {*
    1.11    \begin{matharray}{rcl}
    1.12 -    @{command_def (HOL) "typedecl"} & : & @{text "theory \<rightarrow> theory"} \\
    1.13 -    @{command_def (HOL) "typedef"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
    1.14 +    @{command_def (HOL) "typedef"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
    1.15    \end{matharray}
    1.16  
    1.17    \begin{rail}
    1.18 -    'typedecl' typespec mixfix?
    1.19 -    ;
    1.20      'typedef' altname? abstype '=' repset
    1.21      ;
    1.22  
    1.23 @@ -28,23 +25,25 @@
    1.24  
    1.25    \begin{description}
    1.26    
    1.27 -  \item @{command (HOL) "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} is similar
    1.28 -  to the original @{command "typedecl"} of Isabelle/Pure (see
    1.29 -  \secref{sec:types-pure}), but also declares type arity @{text "t ::
    1.30 -  (type, \<dots>, type) type"}, making @{text t} an actual HOL type
    1.31 -  constructor.  %FIXME check, update
    1.32 +  \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"}
    1.33 +  axiomatizes a Gordon/HOL-style type definition in the background
    1.34 +  theory of the current context, depending on a non-emptiness result
    1.35 +  of the set @{text A} (which needs to be proven interactively).
    1.36 +
    1.37 +  The raw type may not depend on parameters or assumptions of the
    1.38 +  context --- this is logically impossible in Isabelle/HOL --- but the
    1.39 +  non-emptiness property can be local, potentially resulting in
    1.40 +  multiple interpretations in target contexts.  Thus the established
    1.41 +  bijection between the representing set @{text A} and the new type
    1.42 +  @{text t} may semantically depend on local assumptions.
    1.43    
    1.44 -  \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"} sets up
    1.45 -  a goal stating non-emptiness of the set @{text A}.  After finishing
    1.46 -  the proof, the theory will be augmented by a Gordon/HOL-style type
    1.47 -  definition, which establishes a bijection between the representing
    1.48 -  set @{text A} and the new type @{text t}.
    1.49 -  
    1.50 -  Technically, @{command (HOL) "typedef"} defines both a type @{text
    1.51 -  t} and a set (term constant) of the same name (an alternative base
    1.52 -  name may be given in parentheses).  The injection from type to set
    1.53 -  is called @{text Rep_t}, its inverse @{text Abs_t} (this may be
    1.54 -  changed via an explicit @{keyword (HOL) "morphisms"} declaration).
    1.55 +  By default, @{command (HOL) "typedef"} defines both a type @{text t}
    1.56 +  and a set (term constant) of the same name, unless an alternative
    1.57 +  base name is given in parentheses, or the ``@{text "(open)"}''
    1.58 +  declaration is used to suppress a separate constant definition
    1.59 +  altogether.  The injection from type to set is called @{text Rep_t},
    1.60 +  its inverse @{text Abs_t} --- this may be changed via an explicit
    1.61 +  @{keyword (HOL) "morphisms"} declaration.
    1.62    
    1.63    Theorems @{text Rep_t}, @{text Rep_t_inverse}, and @{text
    1.64    Abs_t_inverse} provide the most basic characterization as a
    1.65 @@ -57,19 +56,11 @@
    1.66    on surjectivity; these are already declared as set or type rules for
    1.67    the generic @{method cases} and @{method induct} methods.
    1.68    
    1.69 -  An alternative name may be specified in parentheses; the default is
    1.70 -  to use @{text t} as indicated before.  The ``@{text "(open)"}''
    1.71 -  declaration suppresses a separate constant definition for the
    1.72 -  representing set.
    1.73 +  An alternative name for the set definition (and other derived
    1.74 +  entities) may be specified in parentheses; the default is to use
    1.75 +  @{text t} as indicated before.
    1.76  
    1.77    \end{description}
    1.78 -
    1.79 -  Note that raw type declarations are rarely used in practice; the
    1.80 -  main application is with experimental (or even axiomatic!) theory
    1.81 -  fragments.  Instead of primitive HOL type definitions, user-level
    1.82 -  theories usually refer to higher-level packages such as @{command
    1.83 -  (HOL) "record"} (see \secref{sec:hol-record}) or @{command (HOL)
    1.84 -  "datatype"} (see \secref{sec:hol-datatype}).
    1.85  *}
    1.86  
    1.87  
    1.88 @@ -906,7 +897,7 @@
    1.89  *}
    1.90  
    1.91  
    1.92 -section {* Invoking automated reasoning tools -- The Sledgehammer *}
    1.93 +section {* Invoking automated reasoning tools --- The Sledgehammer *}
    1.94  
    1.95  text {*
    1.96    Isabelle/HOL includes a generic \emph{ATP manager} that allows