# HG changeset patch
# User clasohm
# Date 818357793 -3600
# Node ID fbe857ddc80de7c11a8ebfad9f6de6a484796b00
# Parent  7705e62118659ca927dd3240e2602ff2bd30bd99
removed quotes from consts and syntax sections

diff -r 7705e6211865 -r fbe857ddc80d doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Thu Dec 07 14:25:45 1995 +0100
+++ b/doc-src/Logics/HOL.tex	Thu Dec 07 18:36:33 1995 +0100
@@ -1477,7 +1477,7 @@
 by asserting their reduction rules as new axioms, e.g.\
 \begin{ttbox}
 Append = MyList +
-consts app :: "['a list,'a list] => 'a list"
+consts app :: ['a list,'a list] => 'a list
 rules 
    app_Nil   "app [] ys = ys"
    app_Cons  "app (x#xs) ys = x#app xs ys"
@@ -1488,7 +1488,7 @@
 datatypes can be defined with a special syntax:
 \begin{ttbox}
 Append = MyList +
-consts app :: "'['a list,'a list] => 'a list"
+consts app :: ['a list,'a list] => 'a list
 primrec app MyList.list
    app_Nil   "app [] ys = ys"
    app_Cons  "app (x#xs) ys = x#app xs ys"
@@ -1541,7 +1541,7 @@
 The primitive recursive function can also use infix or mixfix syntax:
 \begin{ttbox}
 Append = MyList +
-consts "@"  :: "['a list,'a list] => 'a list"  (infixr 60)
+consts "@"  :: ['a list,'a list] => 'a list  (infixr 60)
 primrec "op @" MyList.list
    app_Nil   "[] @ ys = ys"
    app_Cons  "(x#xs) @ ys = x#(xs @ ys)"
@@ -1561,7 +1561,7 @@
 %Note that underdefined primitive recursive functions are allowed:
 %\begin{ttbox}
 %Tl = MyList +
-%consts tl  :: "'a list => 'a list"
+%consts tl  :: 'a list => 'a list
 %primrec tl MyList.list
 %   tl_Cons "tl(x#xs) = xs"
 %end
@@ -1708,7 +1708,7 @@
 operator.  First we declare the constant~{\tt Fin}.  Then we declare it
 inductively, with two introduction rules:
 \begin{ttbox}
-consts Fin :: "'a set => 'a set set"
+consts Fin :: 'a set => 'a set set
 inductive "Fin A"
   intrs
     emptyI  "{} : Fin A"