--- 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)"
--- 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
--- 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)"
--- 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"
--- 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"
--- 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
--- 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)"