--- a/doc-src/Intro/advanced.tex Wed Dec 06 14:53:55 1995 +0100
+++ b/doc-src/Intro/advanced.tex Thu Dec 07 14:24:32 1995 +0100
@@ -395,17 +395,18 @@
Most theories simply declare constants, definitions and rules. The {\bf
constant declaration part} has the form
\begin{ttbox}
-consts \(c@1\) :: "\(\tau@1\)"
+consts \(c@1\) :: \(\tau@1\)
\vdots
- \(c@n\) :: "\(\tau@n\)"
+ \(c@n\) :: \(\tau@n\)
\end{ttbox}
where $c@1$, \ldots, $c@n$ are constants and $\tau@1$, \ldots, $\tau@n$ are
-types. Each type {\em must\/} be enclosed in quotation marks. Each
+types. The types must be enclosed in quotation marks if they contain
+user-declared infix type constructors like {\tt *}. Each
constant must be enclosed in quotation marks unless it is a valid
identifier. To declare $c@1$, \ldots, $c@n$ as constants of type $\tau$,
the $n$ declarations may be abbreviated to a single line:
\begin{ttbox}
- \(c@1\), \ldots, \(c@n\) :: "\(\tau\)"
+ \(c@1\), \ldots, \(c@n\) :: \(\tau\)
\end{ttbox}
The {\bf rule declaration part} has the form
\begin{ttbox}
@@ -431,7 +432,7 @@
{\em nand} and {\em xor}:
\begin{ttbox}
Gate = FOL +
-consts nand,xor :: "[o,o] => o"
+consts nand,xor :: [o,o] => o
defs nand_def "nand(P,Q) == ~(P & Q)"
xor_def "xor(P,Q) == P & ~Q | ~P & Q"
end
@@ -493,7 +494,7 @@
Bool = FOL +
types bool
arities bool :: term
-consts tt,ff :: "bool"
+consts tt,ff :: bool
end
\end{ttbox}
A $k$-place type constructor may have arities of the form
@@ -521,8 +522,8 @@
List = FOL +
types 'a list
arities list :: (term)term
-consts Nil :: "'a list"
- Cons :: "['a, 'a list] => 'a list"
+consts Nil :: 'a list
+ Cons :: ['a, 'a list] => 'a list
end
\end{ttbox}
Multiple arity declarations may be abbreviated to a single line:
@@ -541,15 +542,15 @@
to those found in \ML. Such synonyms are defined in the type declaration part
and are fairly self explanatory:
\begin{ttbox}
-types gate = "[o,o] => o"
- 'a pred = "'a => o"
- ('a,'b)nuf = "'b => 'a"
+types gate = [o,o] => o
+ 'a pred = 'a => o
+ ('a,'b)nuf = 'b => 'a
\end{ttbox}
Type declarations and synonyms can be mixed arbitrarily:
\begin{ttbox}
types nat
- 'a stream = "nat => 'a"
- signal = "nat stream"
+ 'a stream = nat => 'a
+ signal = nat stream
'a list
\end{ttbox}
A synonym is merely an abbreviation for some existing type expression. Hence
@@ -558,8 +559,8 @@
to improve the readability of theories. Synonyms can be used just like any
other type:
\begin{ttbox}
-consts and,or :: "gate"
- negate :: "signal => signal"
+consts and,or :: gate
+ negate :: signal => signal
\end{ttbox}
\subsection{Infix and mixfix operators}
@@ -569,8 +570,8 @@
following theory:
\begin{ttbox}
Gate2 = FOL +
-consts "~&" :: "[o,o] => o" (infixl 35)
- "#" :: "[o,o] => o" (infixl 30)
+consts "~&" :: [o,o] => o (infixl 35)
+ "#" :: [o,o] => o (infixl 30)
defs nand_def "P ~& Q == ~(P & Q)"
xor_def "P # Q == P & ~Q | ~P & Q"
end
@@ -590,7 +591,7 @@
{\bf Mixfix} operators may have arbitrary context-free syntaxes. Let us
add a line to the constant declaration part:
\begin{ttbox}
- If :: "[o,o,o] => o" ("if _ then _ else _")
+ If :: [o,o,o] => o ("if _ then _ else _")
\end{ttbox}
This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt
if~$P$ then~$Q$ else~$R$} as well as {\tt If($P$,$Q$,$R$)}. Underscores
@@ -607,7 +608,7 @@
Mixfix declarations can be annotated with priorities, just like
infixes. The example above is just a shorthand for
\begin{ttbox}
- If :: "[o,o,o] => o" ("if _ then _ else _" [0,0,0] 1000)
+ If :: [o,o,o] => o ("if _ then _ else _" [0,0,0] 1000)
\end{ttbox}
The numeric components determine priorities. The list of integers
defines, for each argument position, the minimal priority an expression
@@ -617,7 +618,7 @@
appear everywhere because 1000 is the highest priority. On the other
hand, the declaration
\begin{ttbox}
- If :: "[o,o,o] => o" ("if _ then _ else _" [100,0,0] 99)
+ If :: [o,o,o] => o ("if _ then _ else _" [100,0,0] 99)
\end{ttbox}
defines concrete syntax for a conditional whose first argument cannot have
the form {\tt if~$P$ then~$Q$ else~$R$} because it must have a priority
@@ -675,9 +676,9 @@
\begin{ttbox}
Arith = FOL +
classes arith < term
-consts "0" :: "'a::arith" ("0")
- "1" :: "'a::arith" ("1")
- "+" :: "['a::arith,'a] => 'a" (infixl 60)
+consts "0" :: 'a::arith ("0")
+ "1" :: 'a::arith ("1")
+ "+" :: ['a::arith,'a] => 'a (infixl 60)
end
\end{ttbox}
No rules are declared for these constants: we merely introduce their
@@ -693,7 +694,7 @@
BoolNat = Arith +
types bool nat
arities bool, nat :: arith
-consts Suc :: "nat=>nat"
+consts Suc :: nat=>nat
\ttbreak
rules add0 "0 + n = n::nat"
addS "Suc(m)+n = Suc(m+n)"
@@ -785,10 +786,10 @@
Nat = FOL +
types nat
arities nat :: term
-consts "0" :: "nat" ("0")
- Suc :: "nat=>nat"
- rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
- "+" :: "[nat, nat] => nat" (infixl 60)
+consts "0" :: nat ("0")
+ Suc :: nat=>nat
+ rec :: [nat, 'a, [nat,'a]=>'a] => 'a
+ "+" :: [nat, nat] => nat (infixl 60)
rules Suc_inject "Suc(m)=Suc(n) ==> m=n"
Suc_neq_0 "Suc(m)=0 ==> R"
induct "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
@@ -1077,10 +1078,10 @@
Prolog = FOL +
types 'a list
arities list :: (term)term
-consts Nil :: "'a list"
- ":" :: "['a, 'a list]=> 'a list" (infixr 60)
- app :: "['a list, 'a list, 'a list] => o"
- rev :: "['a list, 'a list] => o"
+consts Nil :: 'a list
+ ":" :: ['a, 'a list]=> 'a list (infixr 60)
+ app :: ['a list, 'a list, 'a list] => o
+ rev :: ['a list, 'a list] => o
rules appNil "app(Nil,ys,ys)"
appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
revNil "rev(Nil,Nil)"
--- a/doc-src/Ref/defining.tex Wed Dec 06 14:53:55 1995 +0100
+++ b/doc-src/Ref/defining.tex Thu Dec 07 14:24:32 1995 +0100
@@ -487,10 +487,10 @@
types
exp
syntax
- "0" :: "exp" ("0" 9)
- "+" :: "[exp, exp] => exp" ("_ + _" [0, 1] 0)
- "*" :: "[exp, exp] => exp" ("_ * _" [3, 2] 2)
- "-" :: "exp => exp" ("- _" [3] 3)
+ "0" :: exp ("0" 9)
+ "+" :: [exp, exp] => exp ("_ + _" [0, 1] 0)
+ "*" :: [exp, exp] => exp ("_ * _" [3, 2] 2)
+ "-" :: exp => exp ("- _" [3] 3)
end
\end{ttbox}
If you put this into a file {\tt EXP.thy} and load it via {\tt use_thy"EXP"},
@@ -578,16 +578,16 @@
Infix operators associating to the left or right can be declared
using {\tt infixl} or {\tt infixr}.
-Roughly speaking, the form {\tt $c$ ::\ "$\sigma$" (infixl $p$)}
+Roughly speaking, the form {\tt $c$ ::\ $\sigma$ (infixl $p$)}
abbreviates the mixfix declarations
\begin{ttbox}
-"op \(c\)" :: "\(\sigma\)" ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\))
-"op \(c\)" :: "\(\sigma\)" ("op \(c\)")
+"op \(c\)" :: \(\sigma\) ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\))
+"op \(c\)" :: \(\sigma\) ("op \(c\)")
\end{ttbox}
-and {\tt $c$ ::\ "$\sigma$" (infixr $p$)} abbreviates the mixfix declarations
+and {\tt $c$ ::\ $\sigma$ (infixr $p$)} abbreviates the mixfix declarations
\begin{ttbox}
-"op \(c\)" :: "\(\sigma\)" ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\))
-"op \(c\)" :: "\(\sigma\)" ("op \(c\)")
+"op \(c\)" :: \(\sigma\) ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\))
+"op \(c\)" :: \(\sigma\) ("op \(c\)")
\end{ttbox}
The infix operator is declared as a constant with the prefix {\tt op}.
Thus, prefixing infixes with \sdx{op} makes them behave like ordinary
@@ -602,7 +602,7 @@
A {\bf binder} is a variable-binding construct such as a quantifier. The
constant declaration
\begin{ttbox}
-\(c\) :: "\(\sigma\)" (binder "\(\Q\)" [\(pb\)] \(p\))
+\(c\) :: \(\sigma\) (binder "\(\Q\)" [\(pb\)] \(p\))
\end{ttbox}
introduces a constant~$c$ of type~$\sigma$, which must have the form
$(\tau@1 \To \tau@2) \To \tau@3$. Its concrete syntax is $\Q~x.P$, where
@@ -613,8 +613,8 @@
The declaration is expanded internally to something like
\begin{ttbox}
-\(c\) :: "(\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)"
-"\(\Q\)"\hskip-3pt :: "[idts, \(\tau@2\)] => \(\tau@3\)" ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\))
+\(c\) :: (\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)
+"\(\Q\)"\hskip-3pt :: [idts, \(\tau@2\)] => \(\tau@3\) ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\))
\end{ttbox}
Here \ndx{idts} is the nonterminal symbol for a list of identifiers with
\index{type constraints}
@@ -631,7 +631,7 @@
\medskip
For example, let us declare the quantifier~$\forall$:\index{quantifiers}
\begin{ttbox}
-All :: "('a => o) => o" (binder "ALL " 10)
+All :: ('a => o) => o (binder "ALL " 10)
\end{ttbox}
This lets us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL
$x$.$P$}. When printing, Isabelle prefers the latter form, but must fall
@@ -712,7 +712,7 @@
arities
o :: logic
consts
- Trueprop :: "o => prop" ("_" 5)
+ Trueprop :: o => prop ("_" 5)
end
\end{ttbox}
The constant \cdx{Trueprop} (the name is arbitrary) acts as an invisible
@@ -725,7 +725,7 @@
\begin{ttbox}
Hilbert = Base +
consts
- "-->" :: "[o, o] => o" (infixr 10)
+ "-->" :: [o, o] => o (infixr 10)
rules
K "P --> Q --> P"
S "(P --> Q --> R) --> (P --> Q) --> P --> R"
@@ -775,7 +775,7 @@
\begin{ttbox}
MinI = Base +
consts
- "-->" :: "[o, o] => o" (infixr 10)
+ "-->" :: [o, o] => o (infixr 10)
rules
impI "(P ==> Q) ==> P --> Q"
impE "[| P --> Q; P |] ==> Q"
@@ -792,7 +792,7 @@
\begin{ttbox}
MinIF = MinI +
consts
- False :: "o"
+ False :: o
rules
FalseE "False ==> P"
end
@@ -801,7 +801,7 @@
\begin{ttbox}
MinC = Base +
consts
- "&" :: "[o, o] => o" (infixr 30)
+ "&" :: [o, o] => o (infixr 30)
\ttbreak
rules
conjI "[| P; Q |] ==> P & Q"
--- a/doc-src/Ref/simplifier.tex Wed Dec 06 14:53:55 1995 +0100
+++ b/doc-src/Ref/simplifier.tex Thu Dec 07 14:24:32 1995 +0100
@@ -515,7 +515,7 @@
Arith} using a theory file:
\begin{ttbox}
NatSum = Arith +
-consts sum :: "[nat=>nat, nat] => nat"
+consts sum :: [nat=>nat, nat] => nat
rules sum_0 "sum(f,0) = 0"
sum_Suc "sum(f,Suc(n)) = f(n) + sum(f,n)"
end
--- a/doc-src/Ref/syntax.tex Wed Dec 06 14:53:55 1995 +0100
+++ b/doc-src/Ref/syntax.tex Thu Dec 07 14:24:32 1995 +0100
@@ -356,14 +356,14 @@
arities
i, o :: logic
consts
- Trueprop :: "o => prop" ("_" 5)
- Collect :: "[i, i => o] => i"
- Replace :: "[i, [i, i] => o] => i"
- Ball :: "[i, i => o] => o"
+ Trueprop :: o => prop ("_" 5)
+ Collect :: [i, i => o] => i
+ Replace :: [i, [i, i] => o] => i
+ Ball :: [i, i => o] => o
syntax
- "{\at}Collect" :: "[idt, i, o] => i" ("(1{\ttlbrace}_:_./ _{\ttrbrace})")
- "{\at}Replace" :: "[idt, idt, i, o] => i" ("(1{\ttlbrace}_./ _:_, _{\ttrbrace})")
- "{\at}Ball" :: "[idt, i, o] => o" ("(3ALL _:_./ _)" 10)
+ "{\at}Collect" :: [idt, i, o] => i ("(1{\ttlbrace}_:_./ _{\ttrbrace})")
+ "{\at}Replace" :: [idt, idt, i, o] => i ("(1{\ttlbrace}_./ _:_, _{\ttrbrace})")
+ "{\at}Ball" :: [idt, i, o] => o ("(3ALL _:_./ _)" 10)
translations
"{\ttlbrace}x:A. P{\ttrbrace}" == "Collect(A, \%x. P)"
"{\ttlbrace}y. x:A, Q{\ttrbrace}" == "Replace(A, \%x y. Q)"
@@ -542,9 +542,9 @@
types
Nil
consts
- Nil :: "'a list"
+ Nil :: 'a list
syntax
- "[]" :: "'a list" ("[]")
+ "[]" :: 'a list ("[]")
translations
"[]" == "Nil"
\end{ttbox}
@@ -578,13 +578,13 @@
types
is
syntax
- "" :: "i => is" ("_")
- "{\at}Enum" :: "[i, is] => is" ("_,/ _")
+ "" :: i => is ("_")
+ "{\at}Enum" :: [i, is] => is ("_,/ _")
consts
- empty :: "i" ("{\ttlbrace}{\ttrbrace}")
- insert :: "[i, i] => i"
+ empty :: i ("{\ttlbrace}{\ttrbrace}")
+ insert :: [i, i] => i
syntax
- "{\at}Finset" :: "is => i" ("{\ttlbrace}(_){\ttrbrace}")
+ "{\at}Finset" :: is => i ("{\ttlbrace}(_){\ttrbrace}")
translations
"{\ttlbrace}x, xs{\ttrbrace}" == "insert(x, {\ttlbrace}xs{\ttrbrace})"
"{\ttlbrace}x{\ttrbrace}" == "insert(x, {\ttlbrace}{\ttrbrace})"
@@ -656,10 +656,10 @@
\begin{ttbox}
PROD = FINSET +
consts
- Pi :: "[i, i => i] => i"
+ Pi :: [i, i => i] => i
syntax
- "{\at}PROD" :: "[idt, i, i] => i" ("(3PROD _:_./ _)" 10)
- "{\at}->" :: "[i, i] => i" ("(_ ->/ _)" [51, 50] 50)
+ "{\at}PROD" :: [idt, i, i] => i ("(3PROD _:_./ _)" 10)
+ "{\at}->" :: [i, i] => i ("(_ ->/ _)" [51, 50] 50)
\ttbreak
translations
"PROD x:A. B" => "Pi(A, \%x. B)"
--- a/doc-src/Ref/theories.tex Wed Dec 06 14:53:55 1995 +0100
+++ b/doc-src/Ref/theories.tex Thu Dec 07 14:24:32 1995 +0100
@@ -68,8 +68,8 @@
indicate the number~$n$.
A {\bf type synonym}\indexbold{type synonyms} is an abbreviation
- $(\alpha@1,\dots,\alpha@n)name = \mbox{\tt"}\tau\mbox{\tt"}$, where
- $name$ can be a string and $\tau$ must be enclosed in quotation marks.
+ $(\alpha@1,\dots,\alpha@n)name = \tau$, where $name$ and $\tau$ can
+ be strings.
\item[$infix$]
declares a type or constant to be an infix operator of priority $nat$