# HG changeset patch
# User clasohm
# Date 815745497 -3600
# Node ID 9b3d3362a0481c716393e7952f352aca7a40ab29
# Parent  9a6e7bd2bfaf37446eae985ee7c9622d9c62a201
removed quotes from types in consts section

diff -r 9a6e7bd2bfaf -r 9b3d3362a048 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Tue Nov 07 12:57:20 1995 +0100
+++ b/src/FOL/IFOL.thy	Tue Nov 07 12:58:17 1995 +0100
@@ -23,28 +23,28 @@
 
 consts
 
-  Trueprop      :: "o => prop"                  ("(_)" 5)
-  True, False   :: "o"
+  Trueprop      :: o => prop                    ("(_)" 5)
+  True, False   :: o
 
   (* Connectives *)
 
-  "="           :: "['a, 'a] => o"              (infixl 50)
+  "="           :: ['a, 'a] => o                (infixl 50)
 
-  Not           :: "o => o"                     ("~ _" [40] 40)
-  "&"           :: "[o, o] => o"                (infixr 35)
-  "|"           :: "[o, o] => o"                (infixr 30)
-  "-->"         :: "[o, o] => o"                (infixr 25)
-  "<->"         :: "[o, o] => o"                (infixr 25)
+  Not           :: o => o                       ("~ _" [40] 40)
+  "&"           :: [o, o] => o                  (infixr 35)
+  "|"           :: [o, o] => o                  (infixr 30)
+  "-->"         :: [o, o] => o                  (infixr 25)
+  "<->"         :: [o, o] => o                  (infixr 25)
 
   (* Quantifiers *)
 
-  All           :: "('a => o) => o"             (binder "ALL " 10)
-  Ex            :: "('a => o) => o"             (binder "EX " 10)
-  Ex1           :: "('a => o) => o"             (binder "EX! " 10)
+  All           :: ('a => o) => o               (binder "ALL " 10)
+  Ex            :: ('a => o) => o               (binder "EX " 10)
+  Ex1           :: ('a => o) => o               (binder "EX! " 10)
 
 
 syntax
-  "~="          :: "['a, 'a] => o"              (infixl 50)
+  "~="          :: ['a, 'a] => o                (infixl 50)
 
 translations
   "x ~= y"      == "~ (x = y)"
diff -r 9a6e7bd2bfaf -r 9b3d3362a048 src/FOL/ex/If.thy
--- a/src/FOL/ex/If.thy	Tue Nov 07 12:57:20 1995 +0100
+++ b/src/FOL/ex/If.thy	Tue Nov 07 12:58:17 1995 +0100
@@ -1,5 +1,5 @@
 If = FOL +
-consts  if     :: "[o,o,o]=>o"
+consts  if     :: [o,o,o]=>o
 rules
         if_def "if(P,Q,R) == P&Q | ~P&R"
 end
diff -r 9a6e7bd2bfaf -r 9b3d3362a048 src/FOL/ex/List.thy
--- a/src/FOL/ex/List.thy	Tue Nov 07 12:57:20 1995 +0100
+++ b/src/FOL/ex/List.thy	Tue Nov 07 12:58:17 1995 +0100
@@ -12,14 +12,14 @@
 arities list :: (term)term
 
 consts
-   hd		:: "'a list => 'a"
-   tl		:: "'a list => 'a list"
-   forall	:: "['a list, 'a => o] => o"
-   len		:: "'a list => nat"
-   at		:: "['a list, nat] => 'a"
-   "[]"		:: "'a list"	("[]")
-   "."		:: "['a, 'a list] => 'a list"  (infixr 80)
-   "++"		:: "['a list, 'a list] => 'a list" (infixr 70)
+   hd		:: 'a list => 'a  
+   tl		:: 'a list => 'a list
+   forall	:: ['a list, 'a => o] => o  
+   len		:: 'a list => nat  
+   at		:: ['a list, nat] => 'a  
+   "[]"		:: ('a list)  	                     ("[]")
+   "."		:: ['a, 'a list] => 'a list          (infixr 80)
+   "++"		:: ['a list, 'a list] => 'a list     (infixr 70)
 
 rules
  list_ind "[| P([]);  ALL x l. P(l)-->P(x.l) |] ==> All(P)"
diff -r 9a6e7bd2bfaf -r 9b3d3362a048 src/FOL/ex/Nat.thy
--- a/src/FOL/ex/Nat.thy	Tue Nov 07 12:57:20 1995 +0100
+++ b/src/FOL/ex/Nat.thy	Tue Nov 07 12:58:17 1995 +0100
@@ -13,10 +13,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   induct      "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)"
         Suc_inject  "Suc(m)=Suc(n) ==> m=n"
         Suc_neq_0   "Suc(m)=0      ==> R"
diff -r 9a6e7bd2bfaf -r 9b3d3362a048 src/FOL/ex/Nat2.thy
--- a/src/FOL/ex/Nat2.thy	Tue Nov 07 12:57:20 1995 +0100
+++ b/src/FOL/ex/Nat2.thy	Tue Nov 07 12:58:17 1995 +0100
@@ -12,10 +12,10 @@
 arities nat :: term
 
 consts
- succ,pred :: "nat => nat"
-       "0" :: "nat"	("0")
-       "+" :: "[nat,nat] => nat" (infixr 90)
-  "<","<=" :: "[nat,nat] => o"   (infixr 70)
+ succ,pred :: nat => nat  
+       "0" :: nat  	("0")
+       "+" :: [nat,nat] => nat   (infixr 90)
+  "<","<=" :: [nat,nat] => o     (infixr 70)
 
 rules
  pred_0		"pred(0) = 0"
diff -r 9a6e7bd2bfaf -r 9b3d3362a048 src/FOL/ex/NatClass.thy
--- a/src/FOL/ex/NatClass.thy	Tue Nov 07 12:57:20 1995 +0100
+++ b/src/FOL/ex/NatClass.thy	Tue Nov 07 12:58:17 1995 +0100
@@ -13,9 +13,9 @@
 NatClass = FOL +
 
 consts
-  "0"           :: "'a"                                 ("0")
-  Suc           :: "'a => 'a"
-  rec           :: "['a, 'a, ['a, 'a] => 'a] => 'a"
+  "0"           :: 'a                                   ("0")
+  Suc           :: 'a => 'a  
+  rec           :: ['a, 'a, ['a, 'a] => 'a] => 'a  
 
 axclass
   nat < term
diff -r 9a6e7bd2bfaf -r 9b3d3362a048 src/FOL/ex/Prolog.thy
--- a/src/FOL/ex/Prolog.thy	Tue Nov 07 12:57:20 1995 +0100
+++ b/src/FOL/ex/Prolog.thy	Tue Nov 07 12:58:17 1995 +0100
@@ -11,10 +11,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)"