1.1 --- a/doc-src/Intro/advanced.tex Wed Dec 06 14:53:55 1995 +0100
1.2 +++ b/doc-src/Intro/advanced.tex Thu Dec 07 14:24:32 1995 +0100
1.3 @@ -395,17 +395,18 @@
1.4 Most theories simply declare constants, definitions and rules. The {\bf
1.5 constant declaration part} has the form
1.6 \begin{ttbox}
1.7 -consts \(c@1\) :: "\(\tau@1\)"
1.8 +consts \(c@1\) :: \(\tau@1\)
1.9 \vdots
1.10 - \(c@n\) :: "\(\tau@n\)"
1.11 + \(c@n\) :: \(\tau@n\)
1.12 \end{ttbox}
1.13 where $c@1$, \ldots, $c@n$ are constants and $\tau@1$, \ldots, $\tau@n$ are
1.14 -types. Each type {\em must\/} be enclosed in quotation marks. Each
1.15 +types. The types must be enclosed in quotation marks if they contain
1.16 +user-declared infix type constructors like {\tt *}. Each
1.17 constant must be enclosed in quotation marks unless it is a valid
1.18 identifier. To declare $c@1$, \ldots, $c@n$ as constants of type $\tau$,
1.19 the $n$ declarations may be abbreviated to a single line:
1.20 \begin{ttbox}
1.21 - \(c@1\), \ldots, \(c@n\) :: "\(\tau\)"
1.22 + \(c@1\), \ldots, \(c@n\) :: \(\tau\)
1.23 \end{ttbox}
1.24 The {\bf rule declaration part} has the form
1.25 \begin{ttbox}
1.26 @@ -431,7 +432,7 @@
1.27 {\em nand} and {\em xor}:
1.28 \begin{ttbox}
1.29 Gate = FOL +
1.30 -consts nand,xor :: "[o,o] => o"
1.31 +consts nand,xor :: [o,o] => o
1.32 defs nand_def "nand(P,Q) == ~(P & Q)"
1.33 xor_def "xor(P,Q) == P & ~Q | ~P & Q"
1.34 end
1.35 @@ -493,7 +494,7 @@
1.36 Bool = FOL +
1.37 types bool
1.38 arities bool :: term
1.39 -consts tt,ff :: "bool"
1.40 +consts tt,ff :: bool
1.41 end
1.42 \end{ttbox}
1.43 A $k$-place type constructor may have arities of the form
1.44 @@ -521,8 +522,8 @@
1.45 List = FOL +
1.46 types 'a list
1.47 arities list :: (term)term
1.48 -consts Nil :: "'a list"
1.49 - Cons :: "['a, 'a list] => 'a list"
1.50 +consts Nil :: 'a list
1.51 + Cons :: ['a, 'a list] => 'a list
1.52 end
1.53 \end{ttbox}
1.54 Multiple arity declarations may be abbreviated to a single line:
1.55 @@ -541,15 +542,15 @@
1.56 to those found in \ML. Such synonyms are defined in the type declaration part
1.57 and are fairly self explanatory:
1.58 \begin{ttbox}
1.59 -types gate = "[o,o] => o"
1.60 - 'a pred = "'a => o"
1.61 - ('a,'b)nuf = "'b => 'a"
1.62 +types gate = [o,o] => o
1.63 + 'a pred = 'a => o
1.64 + ('a,'b)nuf = 'b => 'a
1.65 \end{ttbox}
1.66 Type declarations and synonyms can be mixed arbitrarily:
1.67 \begin{ttbox}
1.68 types nat
1.69 - 'a stream = "nat => 'a"
1.70 - signal = "nat stream"
1.71 + 'a stream = nat => 'a
1.72 + signal = nat stream
1.73 'a list
1.74 \end{ttbox}
1.75 A synonym is merely an abbreviation for some existing type expression. Hence
1.76 @@ -558,8 +559,8 @@
1.77 to improve the readability of theories. Synonyms can be used just like any
1.78 other type:
1.79 \begin{ttbox}
1.80 -consts and,or :: "gate"
1.81 - negate :: "signal => signal"
1.82 +consts and,or :: gate
1.83 + negate :: signal => signal
1.84 \end{ttbox}
1.85
1.86 \subsection{Infix and mixfix operators}
1.87 @@ -569,8 +570,8 @@
1.88 following theory:
1.89 \begin{ttbox}
1.90 Gate2 = FOL +
1.91 -consts "~&" :: "[o,o] => o" (infixl 35)
1.92 - "#" :: "[o,o] => o" (infixl 30)
1.93 +consts "~&" :: [o,o] => o (infixl 35)
1.94 + "#" :: [o,o] => o (infixl 30)
1.95 defs nand_def "P ~& Q == ~(P & Q)"
1.96 xor_def "P # Q == P & ~Q | ~P & Q"
1.97 end
1.98 @@ -590,7 +591,7 @@
1.99 {\bf Mixfix} operators may have arbitrary context-free syntaxes. Let us
1.100 add a line to the constant declaration part:
1.101 \begin{ttbox}
1.102 - If :: "[o,o,o] => o" ("if _ then _ else _")
1.103 + If :: [o,o,o] => o ("if _ then _ else _")
1.104 \end{ttbox}
1.105 This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt
1.106 if~$P$ then~$Q$ else~$R$} as well as {\tt If($P$,$Q$,$R$)}. Underscores
1.107 @@ -607,7 +608,7 @@
1.108 Mixfix declarations can be annotated with priorities, just like
1.109 infixes. The example above is just a shorthand for
1.110 \begin{ttbox}
1.111 - If :: "[o,o,o] => o" ("if _ then _ else _" [0,0,0] 1000)
1.112 + If :: [o,o,o] => o ("if _ then _ else _" [0,0,0] 1000)
1.113 \end{ttbox}
1.114 The numeric components determine priorities. The list of integers
1.115 defines, for each argument position, the minimal priority an expression
1.116 @@ -617,7 +618,7 @@
1.117 appear everywhere because 1000 is the highest priority. On the other
1.118 hand, the declaration
1.119 \begin{ttbox}
1.120 - If :: "[o,o,o] => o" ("if _ then _ else _" [100,0,0] 99)
1.121 + If :: [o,o,o] => o ("if _ then _ else _" [100,0,0] 99)
1.122 \end{ttbox}
1.123 defines concrete syntax for a conditional whose first argument cannot have
1.124 the form {\tt if~$P$ then~$Q$ else~$R$} because it must have a priority
1.125 @@ -675,9 +676,9 @@
1.126 \begin{ttbox}
1.127 Arith = FOL +
1.128 classes arith < term
1.129 -consts "0" :: "'a::arith" ("0")
1.130 - "1" :: "'a::arith" ("1")
1.131 - "+" :: "['a::arith,'a] => 'a" (infixl 60)
1.132 +consts "0" :: 'a::arith ("0")
1.133 + "1" :: 'a::arith ("1")
1.134 + "+" :: ['a::arith,'a] => 'a (infixl 60)
1.135 end
1.136 \end{ttbox}
1.137 No rules are declared for these constants: we merely introduce their
1.138 @@ -693,7 +694,7 @@
1.139 BoolNat = Arith +
1.140 types bool nat
1.141 arities bool, nat :: arith
1.142 -consts Suc :: "nat=>nat"
1.143 +consts Suc :: nat=>nat
1.144 \ttbreak
1.145 rules add0 "0 + n = n::nat"
1.146 addS "Suc(m)+n = Suc(m+n)"
1.147 @@ -785,10 +786,10 @@
1.148 Nat = FOL +
1.149 types nat
1.150 arities nat :: term
1.151 -consts "0" :: "nat" ("0")
1.152 - Suc :: "nat=>nat"
1.153 - rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
1.154 - "+" :: "[nat, nat] => nat" (infixl 60)
1.155 +consts "0" :: nat ("0")
1.156 + Suc :: nat=>nat
1.157 + rec :: [nat, 'a, [nat,'a]=>'a] => 'a
1.158 + "+" :: [nat, nat] => nat (infixl 60)
1.159 rules Suc_inject "Suc(m)=Suc(n) ==> m=n"
1.160 Suc_neq_0 "Suc(m)=0 ==> R"
1.161 induct "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
1.162 @@ -1077,10 +1078,10 @@
1.163 Prolog = FOL +
1.164 types 'a list
1.165 arities list :: (term)term
1.166 -consts Nil :: "'a list"
1.167 - ":" :: "['a, 'a list]=> 'a list" (infixr 60)
1.168 - app :: "['a list, 'a list, 'a list] => o"
1.169 - rev :: "['a list, 'a list] => o"
1.170 +consts Nil :: 'a list
1.171 + ":" :: ['a, 'a list]=> 'a list (infixr 60)
1.172 + app :: ['a list, 'a list, 'a list] => o
1.173 + rev :: ['a list, 'a list] => o
1.174 rules appNil "app(Nil,ys,ys)"
1.175 appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
1.176 revNil "rev(Nil,Nil)"