# HG changeset patch
# User paulson
# Date 892117779 -7200
# Node ID c15f46833f7a71845884790ba590f00e59a45db0
# Parent  f8701e067e432b800bde2277bfa15d734f001d9b
Simplified the syntax description; mentioned FOL vs HOL

diff -r f8701e067e43 -r c15f46833f7a doc-src/Intro/getting.tex
--- a/doc-src/Intro/getting.tex	Tue Apr 07 13:46:34 1998 +0200
+++ b/doc-src/Intro/getting.tex	Thu Apr 09 12:29:39 1998 +0200
@@ -17,9 +17,17 @@
 tacticals have function types such as {\tt tactic->tactic}.  Isabelle
 users can operate on these data structures by writing \ML{} programs.
 
+
 \section{Forward proof}\label{sec:forward} \index{forward proof|(}
 This section describes the concrete syntax for types, terms and theorems,
-and demonstrates forward proof.
+and demonstrates forward proof.  The examples are set in first-order logic.
+The command to start Isabelle running first-order logic is
+\begin{ttbox}
+isabelle FOL
+\end{ttbox}
+Note that just typing \texttt{isabelle} usually brings up higher-order logic
+(\HOL) by default.
+
 
 \subsection{Lexical matters}
 \index{identifiers}\index{reserved words} 
@@ -76,16 +84,15 @@
 \index{*:: symbol}\index{*=> symbol}
 \index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}
 \index{*[ symbol}\index{*] symbol}
-\begin{array}{lll}
-    \multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline
-  \alpha "::" C              & \alpha :: C        & \hbox{class constraint} \\
+\begin{array}{ll}
+    \multicolumn{2}{c}{\hbox{ASCII Notation for Types}} \\ \hline
+  \alpha "::" C              & \hbox{class constraint} \\
   \alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" &
-     \alpha :: \{C@1,\dots,C@n\}             & \hbox{sort constraint} \\
-  \sigma " => " \tau        & \sigma\To\tau & \hbox{function type} \\
-  "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau &
-     [\sigma@1,\ldots,\sigma@n] \To\tau & \hbox{curried function type} \\
-  "(" \tau@1"," \ldots "," \tau@n ")" tycon & 
-     (\tau@1, \ldots, \tau@n)tycon      & \hbox{type construction}
+        \hbox{sort constraint} \\
+  \sigma " => " \tau        & \hbox{function type } \sigma\To\tau \\
+  "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau 
+       & \hbox{$n$-argument function type} \\
+  "(" \tau@1"," \ldots "," \tau@n ")" tycon & \hbox{type construction}
 \end{array} 
 \]
 Terms are those of the typed $\lambda$-calculus.
@@ -93,16 +100,19 @@
 \[\dquotes
 \index{%@{\tt\%} symbol}\index{lambda abs@$\lambda$-abstractions}
 \index{*:: symbol}
-\begin{array}{lll}
-    \multicolumn{3}{c}{\hbox{ASCII Notation for Terms}} \\ \hline
-  t "::" \sigma         & t :: \sigma   & \hbox{type constraint} \\
-  "\%" x "." t          & \lambda x.t   & \hbox{abstraction} \\
-  "\%" x@1\ldots x@n "." t  & \lambda x@1\ldots x@n.t & 
-     \hbox{curried abstraction} \\
-  t "(" u@1"," \ldots "," u@n ")" & 
-  t (u@1, \ldots, u@n) & \hbox{curried application}
+\begin{array}{ll}
+    \multicolumn{2}{c}{\hbox{ASCII Notation for Terms}} \\ \hline
+  t "::" \sigma         & \hbox{type constraint} \\
+  "\%" x "." t          & \hbox{abstraction } \lambda x.t \\
+  "\%" x@1\ldots x@n "." t  & \hbox{abstraction over several arguments} \\
+  t "(" u@1"," \ldots "," u@n ")" &
+     \hbox{application to several arguments (FOL and ZF)} \\
+  t\; u@1 \ldots\; u@n & \hbox{application to several arguments (HOL)}
 \end{array}  
 \]
+Note that \HOL{} uses its traditional ``higher-order'' syntax for application,
+which differs from that used in \FOL\@.
+
 The theorems and rules of an object-logic are represented by theorems in
 the meta-logic, which are expressed using meta-formulae.  Since the
 meta-logic is higher-order, meta-formulae~$\phi$, $\psi$, $\theta$,~\ldots{}
diff -r f8701e067e43 -r c15f46833f7a doc-src/Intro/intro.ind
--- a/doc-src/Intro/intro.ind	Tue Apr 07 13:46:34 1998 +0200
+++ b/doc-src/Intro/intro.ind	Thu Apr 09 12:29:39 1998 +0200
@@ -1,27 +1,27 @@
 \begin{theindex}
 
-  \item {\tt !!} symbol, 25
+  \item {\tt !!} symbol, 26
     \subitem in main goal, 46
   \item {\tt\%} symbol, 25
   \item {\tt ::} symbol, 25
-  \item {\tt ==} symbol, 25
-  \item {\tt ==>} symbol, 25
+  \item {\tt ==} symbol, 26
+  \item {\tt ==>} symbol, 26
   \item {\tt =>} symbol, 25
-  \item {\tt =?=} symbol, 25
+  \item {\tt =?=} symbol, 26
   \item {\tt [} symbol, 25
-  \item {\tt [|} symbol, 25
+  \item {\tt [|} symbol, 26
   \item {\tt ]} symbol, 25
   \item {\tt\ttlbrace} symbol, 25
   \item {\tt\ttrbrace} symbol, 25
-  \item {\tt |]} symbol, 25
+  \item {\tt |]} symbol, 26
 
   \indexspace
 
-  \item {\tt allI} theorem, 37
+  \item {\tt allI} theorem, 38
   \item arities
     \subitem declaring, 4, \bold{49}
   \item {\tt Asm_simp_tac}, 60
-  \item {\tt assume_tac}, 30, 32, 37, 47
+  \item {\tt assume_tac}, 30, 32, 38, 47
   \item assumptions
     \subitem deleting, 20
     \subitem discharge of, 7
@@ -39,13 +39,13 @@
     \subitem Prolog style, 62
   \item {\tt bd}, 31
   \item {\tt be}, 31
-  \item {\tt Blast_tac}, 39
+  \item {\tt Blast_tac}, 39, 40
   \item {\tt br}, 31
-  \item {\tt by}, 30
+  \item {\tt by}, 31
 
   \indexspace
 
-  \item {\tt choplev}, 37, 65
+  \item {\tt choplev}, 37, 38, 65
   \item classes, 3
     \subitem built-in, \bold{25}
   \item classical reasoner, 39
@@ -65,7 +65,7 @@
   \item destruct-resolution, 22, 30
   \item {\tt disjE} theorem, 31
   \item {\tt dres_inst_tac}, 57
-  \item {\tt dresolve_tac}, 30, 32, 33, 38
+  \item {\tt dresolve_tac}, 30, 33, 39
 
   \indexspace
 
@@ -74,22 +74,22 @@
   \item equality
     \subitem polymorphic, 3
   \item {\tt eres_inst_tac}, 57
-  \item {\tt eresolve_tac}, 30, 32, 33, 39, 47
+  \item {\tt eresolve_tac}, 30, 33, 39, 47
   \item examples
     \subitem of deriving rules, 41
     \subitem of induction, 57, 58
     \subitem of simplification, 60
     \subitem of tacticals, 37
     \subitem of theories, 48, 50--54, 56, 61
-    \subitem propositional, 17, 31, 32
-    \subitem with quantifiers, 18, 34, 35, 38
+    \subitem propositional, 17, 31, 33
+    \subitem with quantifiers, 18, 34, 36, 38
   \item {\tt exE} theorem, 38
 
   \indexspace
 
   \item {\tt FalseE} theorem, 45
   \item first-order logic, 1
-  \item flex-flex constraints, 6, 25, \bold{28}
+  \item flex-flex constraints, 6, 26, \bold{29}
   \item {\tt flexflex_rule}, 29
   \item forward proof, 21, 24--30
   \item {\tt fun} type, 1, 4
@@ -132,9 +132,9 @@
   \item {\tt Match} exception, 42
   \item meta-assumptions
     \subitem syntax of, 22
-  \item meta-equality, \bold{5}, 25
-  \item meta-implication, \bold{5}, 7, 25
-  \item meta-quantifiers, \bold{5}, 8, 25
+  \item meta-equality, \bold{5}, 26
+  \item meta-implication, \bold{5}, 7, 26
+  \item meta-quantifiers, \bold{5}, 8, 26
   \item meta-rewriting, 43
   \item mixfix declarations, 52, 53, 56
   \item ML, i
@@ -181,7 +181,7 @@
 
   \item {\tt read_instantiate}, 29
   \item {\tt refl} theorem, 29
-  \item {\tt REPEAT}, 33, 38, 62, 64
+  \item {\tt REPEAT}, 34, 38, 62, 64
   \item {\tt res_inst_tac}, 57, 60
   \item reserved words, 24
   \item resolution, 10, \bold{12}
@@ -213,7 +213,7 @@
   \item simplification sets, 60
   \item sort constraints, 25
   \item sorts, \bold{5}
-  \item {\tt spec} theorem, 28, 36, 37
+  \item {\tt spec} theorem, 28, 36, 38
   \item {\tt standard}, 27
   \item substitution, \bold{8}
   \item {\tt Suc_inject}, 58
@@ -237,10 +237,10 @@
     \subitem defining, 47--57
   \item {\tt thm} ML type, 27
   \item {\tt topthm}, 42
-  \item {\tt Trueprop} constant, 6, 7, 25
+  \item {\tt Trueprop} constant, 6, 7, 26
   \item type constraints, 25
   \item type constructors, 1
-  \item type identifiers, 24
+  \item type identifiers, 25
   \item type synonyms, \bold{51}
   \item types
     \subitem declaring, \bold{49}
@@ -252,12 +252,12 @@
 
   \indexspace
 
-  \item {\tt undo}, 30
+  \item {\tt undo}, 31
   \item unification
     \subitem higher-order, \bold{11}, 58
     \subitem incompleteness of, 11
-  \item unknowns, 10, 24, 34
-    \subitem function, \bold{11}, 28, 34
+  \item unknowns, 10, 25, 34
+    \subitem function, \bold{11}, 29, 34
   \item {\tt use_thy}, \bold{47, 48}
 
   \indexspace