doc-src/Intro/advanced.tex

 \indexbold{constants!declaring}\index{rules!declaring}
 
 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}
 rules   \(id@1\) "\(rule@1\)"
         \vdots

 \index{examples!of theories} 
 This theory extends first-order logic by declaring and defining two constants,
 {\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
 \end{ttbox}
 

 \index{examples!of theories}
 \begin{ttbox}
 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
 $(s@1,\ldots,s@k)c$, where $s@1,\ldots,s@n$ are sorts and $c$ is a class.
 Each sort specifies a type argument; it has the form $\{c@1,\ldots,c@m\}$,

 \index{examples!of theories}
 \begin{ttbox}
 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:
 \begin{ttbox}
 arities \(tycon@1\), \ldots, \(tycon@n\) :: \(arity\)

 \subsection{Type synonyms}\indexbold{type synonyms}
 Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar
 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
 synonyms may not be recursive!  Internally all synonyms are fully expanded.  As
 a consequence Isabelle output never contains synonyms.  Their main purpose is
 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}
 \index{infixes}\index{examples!of theories}
 
 Infix or mixfix syntax may be attached to constants.  Consider the
 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
 \end{ttbox}
 The constant declaration part declares two left-associating infix operators

 
 \bigskip\index{mixfix declarations}
 {\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
 denote argument positions.  
 

     {Chap.\ts\ref{Defining-Logics}}.
 
 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
 at that position must have.  The final integer is the priority of the
 construct itself.  In the example above, any argument expression is
 acceptable because priorities are non-negative, and conditionals may
 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
 of at least~100.  We may of course write
 \begin{quote}\tt

 $term$ and add the three polymorphic constants of this class.
 \index{examples!of theories}\index{constants!overloaded}
 \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
 names without specifying properties.  On the other hand, classes
 with rules make it possible to prove {\bf generic} theorems.  Such

 \index{examples!of theories}
 \begin{ttbox}
 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)"
         nat1        "1 = Suc(0)"
         or0l        "0 + x = x::bool"

 identifier, and could not otherwise be written in terms:
 \begin{ttbox}\index{mixfix declarations}
 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)"
         rec_0       "rec(0,a,f) = a"
         rec_Suc     "rec(Suc(m), a, f) = f(m, rec(m,a,f))"

 rules of~{\tt FOL}.
 \begin{ttbox}
 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)"
         revCons "[| rev(xs,ys); app(ys,x:Nil,zs) |] ==> rev(x:xs,zs)"
 end