--- a/src/HOL/Hoare/Arith2.thy Wed Nov 29 16:58:30 1995 +0100
+++ b/src/HOL/Hoare/Arith2.thy Wed Nov 29 17:01:41 1995 +0100
@@ -9,12 +9,12 @@
Arith2 = Arith +
consts
- divides :: "[nat, nat] => bool" (infixl 70)
- cd :: "[nat, nat, nat] => bool"
- gcd :: "[nat, nat] => nat"
+ divides :: [nat, nat] => bool (infixl 70)
+ cd :: [nat, nat, nat] => bool
+ gcd :: [nat, nat] => nat
- pow :: "[nat, nat] => nat" (infixl 75)
- fac :: "nat => nat"
+ pow :: [nat, nat] => nat (infixl 75)
+ fac :: nat => nat
defs
divides_def "x divides n == 0<n & 0<x & (n mod x) = 0"
--- a/src/HOL/Hoare/Examples.thy Wed Nov 29 16:58:30 1995 +0100
+++ b/src/HOL/Hoare/Examples.thy Wed Nov 29 17:01:41 1995 +0100
@@ -9,8 +9,8 @@
Examples = Hoare + Arith2 +
syntax
- "@1" :: "nat" ("1")
- "@2" :: "nat" ("2")
+ "@1" :: nat ("1")
+ "@2" :: nat ("2")
translations
"1" == "Suc(0)"
--- a/src/HOL/Hoare/Hoare.thy Wed Nov 29 16:58:30 1995 +0100
+++ b/src/HOL/Hoare/Hoare.thy Wed Nov 29 17:01:41 1995 +0100
@@ -17,27 +17,27 @@
'a com = "'a state => 'a state => bool" (* denotation of programs *)
syntax
- "@Skip" :: "'a prog" ("SKIP")
- "@Assign" :: "[id, 'a] => 'a prog" ("_ := _")
- "@Seq" :: "['a prog, 'a prog] => 'a prog" ("_;//_" [0,1000] 999)
- "@If" :: "[bool, 'a prog, 'a prog] => 'a prog"
+ "@Skip" :: 'a prog ("SKIP")
+ "@Assign" :: [id, 'a] => 'a prog ("_ := _")
+ "@Seq" :: ['a prog, 'a prog] => 'a prog ("_;//_" [0,1000] 999)
+ "@If" :: [bool, 'a prog, 'a prog] => 'a prog
("IF _//THEN// (_)//ELSE// (_)//END")
- "@While" :: "[bool, bool, 'a prog] => 'a prog"
+ "@While" :: [bool, bool, 'a prog] => 'a prog
("WHILE _//DO {_}// (_)//END")
- "@Spec" :: "[bool, 'a prog, bool] => bool" ("{_}//_//{_}")
+ "@Spec" :: [bool, 'a prog, bool] => bool ("{_}//_//{_}")
consts
(* semantics *)
- Skip :: "'a com"
- Assign :: "[pvar, 'a exp] => 'a com"
- Seq :: "['a com, 'a com] => 'a com"
- Cond :: "['a bexp, 'a com, 'a com] => 'a com"
- While :: "['a bexp, 'a bexp, 'a com] => 'a com"
- Iter :: "[nat, 'a bexp, 'a com] => 'a com"
+ Skip :: 'a com
+ Assign :: [pvar, 'a exp] => 'a com
+ Seq :: ['a com, 'a com] => 'a com
+ Cond :: ['a bexp, 'a com, 'a com] => 'a com
+ While :: ['a bexp, 'a bexp, 'a com] => 'a com
+ Iter :: [nat, 'a bexp, 'a com] => 'a com
- Spec :: "['a bexp, 'a com, 'a bexp] => bool"
+ Spec :: ['a bexp, 'a com, 'a bexp] => bool
defs
(* denotational semantics *)
--- a/src/HOL/IMP/Com.thy Wed Nov 29 16:58:30 1995 +0100
+++ b/src/HOL/IMP/Com.thy Wed Nov 29 17:01:41 1995 +0100
@@ -26,7 +26,7 @@
(** Evaluation of arithmetic expressions **)
consts evala :: "(aexp*state*nat)set"
- "@evala" :: "[aexp,state,nat] => bool" ("<_,_>/ -a-> _" [0,0,50] 50)
+ "@evala" :: [aexp,state,nat] => bool ("<_,_>/ -a-> _" [0,0,50] 50)
translations
"<ae,sig> -a-> n" == "(ae,sig,n) : evala"
inductive "evala"
@@ -51,7 +51,7 @@
(** Evaluation of boolean expressions **)
consts evalb :: "(bexp*state*bool)set"
- "@evalb" :: "[bexp,state,bool] => bool" ("<_,_>/ -b-> _" [0,0,50] 50)
+ "@evalb" :: [bexp,state,bool] => bool ("<_,_>/ -b-> _" [0,0,50] 50)
translations
"<be,sig> -b-> b" == "(be,sig,b) : evalb"
@@ -79,8 +79,8 @@
(** Execution of commands **)
consts evalc :: "(com*state*state)set"
- "@evalc" :: "[com,state,state] => bool" ("<_,_>/ -c-> _" [0,0,50] 50)
- "assign" :: "[state,nat,loc] => state" ("_[_'/_]" [95,0,0] 95)
+ "@evalc" :: [com,state,state] => bool ("<_,_>/ -c-> _" [0,0,50] 50)
+ "assign" :: [state,nat,loc] => state ("_[_'/_]" [95,0,0] 95)
translations
"<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
--- a/src/HOL/IMP/Denotation.thy Wed Nov 29 16:58:30 1995 +0100
+++ b/src/HOL/IMP/Denotation.thy Wed Nov 29 17:01:41 1995 +0100
@@ -10,10 +10,10 @@
types com_den = "(state*state)set"
consts
- A :: "aexp => state => nat"
- B :: "bexp => state => bool"
- C :: "com => com_den"
- Gamma :: "[bexp,com_den] => (com_den => com_den)"
+ A :: aexp => state => nat
+ B :: bexp => state => bool
+ C :: com => com_den
+ Gamma :: [bexp,com_den] => (com_den => com_den)
primrec A aexp
A_nat "A(N(n)) = (%s. n)"
--- a/src/HOL/IMP/Hoare.thy Wed Nov 29 16:58:30 1995 +0100
+++ b/src/HOL/IMP/Hoare.thy Wed Nov 29 17:01:41 1995 +0100
@@ -8,8 +8,8 @@
Hoare = Denotation +
consts
- spec :: "[state=>bool,com,state=>bool] => bool"
-(* syntax "@spec" :: "[bool,com,bool] => bool" *)
+ spec :: [state=>bool,com,state=>bool] => bool
+(* syntax "@spec" :: [bool,com,bool] => bool *)
("{{(1_)}}/ (_)/ {{(1_)}}" 10)
defs
spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t"
--- a/src/HOL/Integ/Integ.thy Wed Nov 29 16:58:30 1995 +0100
+++ b/src/HOL/Integ/Integ.thy Wed Nov 29 17:01:41 1995 +0100
@@ -23,13 +23,13 @@
int :: {ord, plus, times, minus}
consts
- zNat :: "nat set"
- znat :: "nat => int" ("$# _" [80] 80)
- zminus :: "int => int" ("$~ _" [80] 80)
- znegative :: "int => bool"
- zmagnitude :: "int => int"
- zdiv,zmod :: "[int,int]=>int" (infixl 70)
- zpred,zsuc :: "int=>int"
+ zNat :: nat set
+ znat :: nat => int ("$# _" [80] 80)
+ zminus :: int => int ("$~ _" [80] 80)
+ znegative :: int => bool
+ zmagnitude :: int => int
+ zdiv,zmod :: [int,int]=>int (infixl 70)
+ zpred,zsuc :: int=>int
defs
zNat_def "zNat == {x::nat. True}"
--- a/src/HOL/Lex/Auto.thy Wed Nov 29 16:58:30 1995 +0100
+++ b/src/HOL/Lex/Auto.thy Wed Nov 29 17:01:41 1995 +0100
@@ -17,12 +17,12 @@
types ('a,'b)auto = "'b * ('b => 'a => 'b) * ('b => bool)"
consts
- start :: "('a, 'b)auto => 'b"
- next :: "('a, 'b)auto => ('b => 'a => 'b)"
- fin :: "('a, 'b)auto => ('b => bool)"
- nexts :: "('a, 'b)auto => 'b => 'a list => 'b"
- accepts :: "('a,'b) auto => 'a list => bool"
- acc_prefix :: "('a, 'b)auto => 'b => 'a list => bool"
+ start :: ('a, 'b)auto => 'b
+ next :: ('a, 'b)auto => ('b => 'a => 'b)
+ fin :: ('a, 'b)auto => ('b => bool)
+ nexts :: ('a, 'b)auto => 'b => 'a list => 'b
+ accepts :: ('a,'b) auto => 'a list => bool
+ acc_prefix :: ('a, 'b)auto => 'b => 'a list => bool
defs
start_def "start(A) == fst(A)"
--- a/src/HOL/Lex/AutoChopper.thy Wed Nov 29 16:58:30 1995 +0100
+++ b/src/HOL/Lex/AutoChopper.thy Wed Nov 29 17:01:41 1995 +0100
@@ -17,8 +17,8 @@
AutoChopper = Auto + Chopper +
consts
- is_auto_chopper :: "(('a,'b)auto => 'a chopper) => bool"
- auto_chopper :: "('a,'b)auto => 'a chopper"
+ is_auto_chopper :: (('a,'b)auto => 'a chopper) => bool
+ auto_chopper :: ('a,'b)auto => 'a chopper
acc :: "['a list, 'b, 'a list, 'a list, 'a list list*'a list, ('a,'b)auto]
=> 'a list list * 'a list"
--- a/src/HOL/Lex/Chopper.thy Wed Nov 29 16:58:30 1995 +0100
+++ b/src/HOL/Lex/Chopper.thy Wed Nov 29 17:01:41 1995 +0100
@@ -20,7 +20,7 @@
types 'a chopper = "'a list => 'a list list * 'a list"
consts
- is_longest_prefix_chopper :: "['a list => bool, 'a chopper] => bool"
+ is_longest_prefix_chopper :: ['a list => bool, 'a chopper] => bool
defs
is_longest_prefix_chopper_def
--- a/src/HOL/Subst/UTerm.thy Wed Nov 29 16:58:30 1995 +0100
+++ b/src/HOL/Subst/UTerm.thy Wed Nov 29 17:01:41 1995 +0100
@@ -14,15 +14,15 @@
uterm :: (term)term
consts
- uterm :: "'a item set => 'a item set"
- Rep_uterm :: "'a uterm => 'a item"
- Abs_uterm :: "'a item => 'a uterm"
- VAR :: "'a item => 'a item"
- CONST :: "'a item => 'a item"
- COMB :: "['a item, 'a item] => 'a item"
- Var :: "'a => 'a uterm"
- Const :: "'a => 'a uterm"
- Comb :: "['a uterm, 'a uterm] => 'a uterm"
+ uterm :: 'a item set => 'a item set
+ Rep_uterm :: 'a uterm => 'a item
+ Abs_uterm :: 'a item => 'a uterm
+ VAR :: 'a item => 'a item
+ CONST :: 'a item => 'a item
+ COMB :: ['a item, 'a item] => 'a item
+ Var :: 'a => 'a uterm
+ Const :: 'a => 'a uterm
+ Comb :: ['a uterm, 'a uterm] => 'a uterm
UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b,
['a item , 'a item, 'b, 'b]=>'b] => 'b"
uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b,
--- a/src/HOL/Subst/Unifier.thy Wed Nov 29 16:58:30 1995 +0100
+++ b/src/HOL/Subst/Unifier.thy Wed Nov 29 17:01:41 1995 +0100
@@ -14,7 +14,7 @@
">>" :: "[('a*('a uterm))list,('a*('a uterm))list] => bool" (infixr 52)
MGUnifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
MGIUnifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
- UWFD :: "['a uterm,'a uterm,'a uterm,'a uterm] => bool"
+ UWFD :: ['a uterm,'a uterm,'a uterm,'a uterm] => bool
rules (*Definitions*)