doc-src/IsarImplementation/Thy/logic.thy
 changeset 20493 48fea5e99505 parent 20491 98ba42f19995 child 20494 99ad217b6974
     1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Fri Sep 08 13:33:11 2006 +0200
1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Fri Sep 08 17:33:05 2006 +0200
1.3 @@ -9,7 +9,7 @@
1.4    The logical foundations of Isabelle/Isar are that of the Pure logic,
1.5    which has been introduced as a natural-deduction framework in
1.6    \cite{paulson700}.  This is essentially the same logic as @{text
1.7 -  "\<lambda>HOL"}'' in the more abstract framework of Pure Type Systems (PTS)
1.8 +  "\<lambda>HOL"}'' in the more abstract setting of Pure Type Systems (PTS)
1.9    \cite{Barendregt-Geuvers:2001}, although there are some key
1.10    differences in the specific treatment of simple types in
1.11    Isabelle/Pure.
1.12 @@ -56,26 +56,27 @@
1.13    elements wrt.\ the sort order.
1.14
1.15    \medskip A \emph{fixed type variable} is a pair of a basic name
1.16 -  (starting with @{text "'"} character) and a sort constraint.  For
1.17 +  (starting with a @{text "'"} character) and a sort constraint.  For
1.18    example, @{text "('a, s)"} which is usually printed as @{text
1.19    "\<alpha>\<^isub>s"}.  A \emph{schematic type variable} is a pair of an
1.20    indexname and a sort constraint.  For example, @{text "(('a, 0),
1.21    s)"} which is usually printed as @{text "?\<alpha>\<^isub>s"}.
1.22
1.23    Note that \emph{all} syntactic components contribute to the identity
1.24 -  of type variables, including the literal sort constraint.  The core
1.25 -  logic handles type variables with the same name but different sorts
1.26 -  as different, although some outer layers of the system make it hard
1.27 -  to produce anything like this.
1.28 +  of type variables, including the sort constraint.  The core logic
1.29 +  handles type variables with the same name but different sorts as
1.30 +  different, although some outer layers of the system make it hard to
1.31 +  produce anything like this.
1.32
1.33 -  A \emph{type constructor} is a @{text "k"}-ary operator on types
1.34 -  declared in the theory.  Type constructor application is usually
1.35 -  written postfix.  For @{text "k = 0"} the argument tuple is omitted,
1.36 -  e.g.\ @{text "prop"} instead of @{text "()prop"}.  For @{text "k =
1.37 -  1"} the parentheses are omitted, e.g.\ @{text "\<alpha> list"} instead of
1.38 -  @{text "(\<alpha>)list"}.  Further notation is provided for specific
1.39 -  constructors, notably right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"}
1.40 -  instead of @{text "(\<alpha>, \<beta>)fun"} constructor.
1.41 +  A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}-ary operator
1.42 +  on types declared in the theory.  Type constructor application is
1.43 +  usually written postfix as @{text "(FIXME)\<kappa>"}.  For @{text "k = 0"}
1.44 +  the argument tuple is omitted, e.g.\ @{text "prop"} instead of
1.45 +  @{text "()prop"}.  For @{text "k = 1"} the parentheses are omitted,
1.46 +  e.g.\ @{text "\<alpha> list"} instead of @{text "(\<alpha>)list"}.  Further
1.47 +  notation is provided for specific constructors, notably
1.48 +  right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of @{text "(\<alpha>,
1.49 +  \<beta>)fun"} constructor.
1.50
1.51    A \emph{type} is defined inductively over type variables and type
1.52    constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |