--- a/src/HOL/IOA/ABP/Abschannel.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Abschannel.thy Fri Dec 01 12:03:13 1995 +0100
@@ -14,21 +14,21 @@
consts
-ch_asig :: "'a act signature"
-ch_trans :: "('a act, 'a list)transition set"
-ch_ioa :: "('a act, 'a list)ioa"
+ch_asig :: 'a act signature
+ch_trans :: ('a act, 'a list)transition set
+ch_ioa :: ('a act, 'a list)ioa
-rsch_actions :: "'m action => bool act option"
+rsch_actions :: 'm action => bool act option
srch_actions :: "'m action =>(bool * 'm) act option"
srch_asig,
-rsch_asig :: "'m action signature"
+rsch_asig :: 'm action signature
-srch_trans :: "('m action, 'm packet list)transition set"
-rsch_trans :: "('m action, bool list)transition set"
+srch_trans :: ('m action, 'm packet list)transition set
+rsch_trans :: ('m action, bool list)transition set
-srch_ioa :: "('m action, 'm packet list)ioa"
-rsch_ioa :: "('m action, bool list)ioa"
+srch_ioa :: ('m action, 'm packet list)ioa
+rsch_ioa :: ('m action, bool list)ioa
defs
--- a/src/HOL/IOA/ABP/Abschannel_finite.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Abschannel_finite.thy Fri Dec 01 12:03:13 1995 +0100
@@ -10,22 +10,22 @@
consts
-ch_fin_asig :: "'a act signature"
+ch_fin_asig :: 'a act signature
-ch_fin_trans :: "('a act, 'a list)transition set"
+ch_fin_trans :: ('a act, 'a list)transition set
-ch_fin_ioa :: "('a act, 'a list)ioa"
+ch_fin_ioa :: ('a act, 'a list)ioa
srch_fin_asig,
-rsch_fin_asig :: "'m action signature"
+rsch_fin_asig :: 'm action signature
-srch_fin_trans :: "('m action, 'm packet list)transition set"
-rsch_fin_trans :: "('m action, bool list)transition set"
+srch_fin_trans :: ('m action, 'm packet list)transition set
+rsch_fin_trans :: ('m action, bool list)transition set
-srch_fin_ioa :: "('m action, 'm packet list)ioa"
-rsch_fin_ioa :: "('m action, bool list)ioa"
+srch_fin_ioa :: ('m action, 'm packet list)ioa
+rsch_fin_ioa :: ('m action, bool list)ioa
-reverse :: "'a list => 'a list"
+reverse :: 'a list => 'a list
primrec
reverse List.list
--- a/src/HOL/IOA/ABP/Correctness.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Correctness.thy Fri Dec 01 12:03:13 1995 +0100
@@ -10,9 +10,9 @@
consts
-reduce :: "'a list => 'a list"
+reduce :: 'a list => 'a list
-abs :: "'c"
+abs :: 'c
system_ioa :: "('m action, bool * 'm impl_state)ioa"
system_fin_ioa :: "('m action, bool * 'm impl_state)ioa"
--- a/src/HOL/IOA/ABP/Env.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Env.thy Fri Dec 01 12:03:13 1995 +0100
@@ -16,10 +16,10 @@
consts
-env_asig :: "'m action signature"
-env_trans :: "('m action, 'm env_state)transition set"
-env_ioa :: "('m action, 'm env_state)ioa"
-next :: "'m env_state => bool"
+env_asig :: 'm action signature
+env_trans :: ('m action, 'm env_state)transition set
+env_ioa :: ('m action, 'm env_state)ioa
+next :: 'm env_state => bool
defs
--- a/src/HOL/IOA/ABP/Impl.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Impl.thy Fri Dec 01 12:03:13 1995 +0100
@@ -16,11 +16,11 @@
consts
- impl_ioa :: "('m action, 'm impl_state)ioa"
- sen :: "'m impl_state => 'm sender_state"
- rec :: "'m impl_state => 'm receiver_state"
- srch :: "'m impl_state => 'm packet list"
- rsch :: "'m impl_state => bool list"
+ impl_ioa :: ('m action, 'm impl_state)ioa
+ sen :: 'm impl_state => 'm sender_state
+ rec :: 'm impl_state => 'm receiver_state
+ srch :: 'm impl_state => 'm packet list
+ rsch :: 'm impl_state => bool list
defs
--- a/src/HOL/IOA/ABP/Impl_finite.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Impl_finite.thy Fri Dec 01 12:03:13 1995 +0100
@@ -16,11 +16,11 @@
consts
- impl_fin_ioa :: "('m action, 'm impl_fin_state)ioa"
- sen_fin :: "'m impl_fin_state => 'm sender_state"
- rec_fin :: "'m impl_fin_state => 'm receiver_state"
- srch_fin :: "'m impl_fin_state => 'm packet list"
- rsch_fin :: "'m impl_fin_state => bool list"
+ impl_fin_ioa :: ('m action, 'm impl_fin_state)ioa
+ sen_fin :: 'm impl_fin_state => 'm sender_state
+ rec_fin :: 'm impl_fin_state => 'm receiver_state
+ srch_fin :: 'm impl_fin_state => 'm packet list
+ rsch_fin :: 'm impl_fin_state => bool list
defs
--- a/src/HOL/IOA/ABP/Packet.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Packet.thy Fri Dec 01 12:03:13 1995 +0100
@@ -14,8 +14,8 @@
consts
- hdr :: "'msg packet => bool"
- msg :: "'msg packet => 'msg"
+ hdr :: 'msg packet => bool
+ msg :: 'msg packet => 'msg
defs
--- a/src/HOL/IOA/ABP/Receiver.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Receiver.thy Fri Dec 01 12:03:13 1995 +0100
@@ -16,11 +16,11 @@
consts
- receiver_asig :: "'m action signature"
- receiver_trans:: "('m action, 'm receiver_state)transition set"
- receiver_ioa :: "('m action, 'm receiver_state)ioa"
- rq :: "'m receiver_state => 'm list"
- rbit :: "'m receiver_state => bool"
+ receiver_asig :: 'm action signature
+ receiver_trans:: ('m action, 'm receiver_state)transition set
+ receiver_ioa :: ('m action, 'm receiver_state)ioa
+ rq :: 'm receiver_state => 'm list
+ rbit :: 'm receiver_state => bool
defs
--- a/src/HOL/IOA/ABP/Sender.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Sender.thy Fri Dec 01 12:03:13 1995 +0100
@@ -15,11 +15,11 @@
consts
-sender_asig :: "'m action signature"
-sender_trans :: "('m action, 'm sender_state)transition set"
-sender_ioa :: "('m action, 'm sender_state)ioa"
-sq :: "'m sender_state => 'm list"
-sbit :: "'m sender_state => bool"
+sender_asig :: 'm action signature
+sender_trans :: ('m action, 'm sender_state)transition set
+sender_ioa :: ('m action, 'm sender_state)ioa
+sq :: 'm sender_state => 'm list
+sbit :: 'm sender_state => bool
defs
--- a/src/HOL/IOA/ABP/Spec.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Spec.thy Fri Dec 01 12:03:13 1995 +0100
@@ -10,9 +10,9 @@
consts
-spec_sig :: "'m action signature"
-spec_trans :: "('m action, 'm list)transition set"
-spec_ioa :: "('m action, 'm list)ioa"
+spec_sig :: 'm action signature
+spec_trans :: ('m action, 'm list)transition set
+spec_ioa :: ('m action, 'm list)ioa
defs
--- a/src/HOL/IOA/NTP/Abschannel.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Abschannel.thy Fri Dec 01 12:03:13 1995 +0100
@@ -12,23 +12,23 @@
consts
-ch_asig :: "'a act signature"
+ch_asig :: 'a act signature
-ch_trans :: "('a act, 'a multiset)transition set"
+ch_trans :: ('a act, 'a multiset)transition set
-ch_ioa :: "('a act, 'a multiset)ioa"
+ch_ioa :: ('a act, 'a multiset)ioa
-rsch_actions :: "'m action => bool act option"
+rsch_actions :: 'm action => bool act option
srch_actions :: "'m action =>(bool * 'm) act option"
srch_asig,
-rsch_asig :: "'m action signature"
+rsch_asig :: 'm action signature
-srch_trans :: "('m action, 'm packet multiset)transition set"
-rsch_trans :: "('m action, bool multiset)transition set"
+srch_trans :: ('m action, 'm packet multiset)transition set
+rsch_trans :: ('m action, bool multiset)transition set
-srch_ioa :: "('m action, 'm packet multiset)ioa"
-rsch_ioa :: "('m action, bool multiset)ioa"
+srch_ioa :: ('m action, 'm packet multiset)ioa
+rsch_ioa :: ('m action, bool multiset)ioa
defs
--- a/src/HOL/IOA/NTP/Correctness.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Correctness.thy Fri Dec 01 12:03:13 1995 +0100
@@ -10,7 +10,7 @@
consts
-hom :: "'m impl_state => 'm list"
+hom :: 'm impl_state => 'm list
defs
--- a/src/HOL/IOA/NTP/Impl.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Impl.thy Fri Dec 01 12:03:13 1995 +0100
@@ -16,14 +16,14 @@
consts
- impl_ioa :: "('m action, 'm impl_state)ioa"
- sen :: "'m impl_state => 'm sender_state"
- rec :: "'m impl_state => 'm receiver_state"
- srch :: "'m impl_state => 'm packet multiset"
- rsch :: "'m impl_state => bool multiset"
+ impl_ioa :: ('m action, 'm impl_state)ioa
+ sen :: 'm impl_state => 'm sender_state
+ rec :: 'm impl_state => 'm receiver_state
+ srch :: 'm impl_state => 'm packet multiset
+ rsch :: 'm impl_state => bool multiset
inv1, inv2,
- inv3, inv4 :: "'m impl_state => bool"
- hdr_sum :: "'m packet multiset => bool => nat"
+ inv3, inv4 :: 'm impl_state => bool
+ hdr_sum :: 'm packet multiset => bool => nat
defs
--- a/src/HOL/IOA/NTP/Multiset.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Multiset.thy Fri Dec 01 12:03:13 1995 +0100
@@ -19,11 +19,11 @@
consts
- "{|}" :: "'a multiset" ("{|}")
- addm :: "['a multiset, 'a] => 'a multiset"
- delm :: "['a multiset, 'a] => 'a multiset"
- countm :: "['a multiset, 'a => bool] => nat"
- count :: "['a multiset, 'a] => nat"
+ "{|}" :: 'a multiset ("{|}")
+ addm :: ['a multiset, 'a] => 'a multiset
+ delm :: ['a multiset, 'a] => 'a multiset
+ countm :: ['a multiset, 'a => bool] => nat
+ count :: ['a multiset, 'a] => nat
rules
--- a/src/HOL/IOA/NTP/Packet.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Packet.thy Fri Dec 01 12:03:13 1995 +0100
@@ -14,8 +14,8 @@
consts
- hdr :: "'msg packet => bool"
- msg :: "'msg packet => 'msg"
+ hdr :: 'msg packet => bool
+ msg :: 'msg packet => 'msg
defs
--- a/src/HOL/IOA/NTP/Receiver.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Receiver.thy Fri Dec 01 12:03:13 1995 +0100
@@ -16,14 +16,14 @@
consts
- receiver_asig :: "'m action signature"
- receiver_trans:: "('m action, 'm receiver_state)transition set"
- receiver_ioa :: "('m action, 'm receiver_state)ioa"
- rq :: "'m receiver_state => 'm list"
- rsent :: "'m receiver_state => bool multiset"
- rrcvd :: "'m receiver_state => 'm packet multiset"
- rbit :: "'m receiver_state => bool"
- rsending :: "'m receiver_state => bool"
+ receiver_asig :: 'm action signature
+ receiver_trans:: ('m action, 'm receiver_state)transition set
+ receiver_ioa :: ('m action, 'm receiver_state)ioa
+ rq :: 'm receiver_state => 'm list
+ rsent :: 'm receiver_state => bool multiset
+ rrcvd :: 'm receiver_state => 'm packet multiset
+ rbit :: 'm receiver_state => bool
+ rsending :: 'm receiver_state => bool
defs
--- a/src/HOL/IOA/NTP/Sender.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Sender.thy Fri Dec 01 12:03:13 1995 +0100
@@ -15,13 +15,13 @@
consts
-sender_asig :: "'m action signature"
-sender_trans :: "('m action, 'm sender_state)transition set"
-sender_ioa :: "('m action, 'm sender_state)ioa"
-sq :: "'m sender_state => 'm list"
-ssent,srcvd :: "'m sender_state => bool multiset"
-sbit :: "'m sender_state => bool"
-ssending :: "'m sender_state => bool"
+sender_asig :: 'm action signature
+sender_trans :: ('m action, 'm sender_state)transition set
+sender_ioa :: ('m action, 'm sender_state)ioa
+sq :: 'm sender_state => 'm list
+ssent,srcvd :: 'm sender_state => bool multiset
+sbit :: 'm sender_state => bool
+ssending :: 'm sender_state => bool
defs
--- a/src/HOL/IOA/NTP/Spec.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Spec.thy Fri Dec 01 12:03:13 1995 +0100
@@ -10,9 +10,9 @@
consts
-spec_sig :: "'m action signature"
-spec_trans :: "('m action, 'm list)transition set"
-spec_ioa :: "('m action, 'm list)ioa"
+spec_sig :: 'm action signature
+spec_trans :: ('m action, 'm list)transition set
+spec_ioa :: ('m action, 'm list)ioa
defs
--- a/src/HOL/Lambda/Eta.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/Lambda/Eta.thy Fri Dec 01 12:03:13 1995 +0100
@@ -7,11 +7,11 @@
*)
Eta = ParRed + Commutation +
-consts free :: "db => nat => bool"
- decr :: "[db,nat] => db"
+consts free :: db => nat => bool
+ decr :: [db,nat] => db
eta :: "(db * db) set"
-syntax "-e>", "-e>>", "-e>=" , "->=" :: "[db,db] => bool" (infixl 50)
+syntax "-e>", "-e>>", "-e>=" , "->=" :: [db,db] => bool (infixl 50)
translations
"s -e> t" == "(s,t) : eta"
--- a/src/HOL/Lambda/Lambda.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/Lambda/Lambda.thy Fri Dec 01 12:03:13 1995 +0100
@@ -12,11 +12,11 @@
datatype db = Var nat | "@" db db (infixl 200) | Fun db
consts
- subst :: "[db,db,nat]=>db" ("_[_'/_]" [300,0,0] 300)
- lift :: "[db,nat] => db"
+ subst :: [db,db,nat]=>db ("_[_'/_]" [300,0,0] 300)
+ lift :: [db,nat] => db
(* optimized versions *)
- substn :: "[db,db,nat] => db"
- liftn :: "[nat,db,nat] => db"
+ substn :: [db,db,nat] => db
+ liftn :: [nat,db,nat] => db
primrec lift db
lift_Var "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
@@ -42,7 +42,7 @@
consts beta :: "(db * db) set"
-syntax "->", "->>" :: "[db,db] => bool" (infixl 50)
+syntax "->", "->>" :: [db,db] => bool (infixl 50)
translations
"s -> t" == "(s,t) : beta"
--- a/src/HOL/Lambda/ParRed.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/Lambda/ParRed.thy Fri Dec 01 12:03:13 1995 +0100
@@ -10,7 +10,7 @@
consts par_beta :: "(db * db) set"
-syntax "=>" :: "[db,db] => bool" (infixl 50)
+syntax "=>" :: [db,db] => bool (infixl 50)
translations
"s => t" == "(s,t) : par_beta"
@@ -23,8 +23,8 @@
beta "[| s => s'; t => t' |] ==> (Fun s) @ t => s'[t'/0]"
consts
- cd :: "db => db"
- deFun :: "db => db"
+ cd :: db => db
+ deFun :: db => db
primrec cd db
cd_Var "cd(Var n) = Var n"
--- a/src/HOL/MiniML/I.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/MiniML/I.thy Fri Dec 01 12:03:13 1995 +0100
@@ -8,7 +8,7 @@
I = W +
consts
- I :: "[expr, type_expr list, nat, subst] => result_W"
+ I :: [expr, type_expr list, nat, subst] => result_W
primrec I expr
I_Var "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
--- a/src/HOL/MiniML/Maybe.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/MiniML/Maybe.thy Fri Dec 01 12:03:13 1995 +0100
@@ -10,7 +10,7 @@
datatype 'a maybe = Ok 'a | Fail
-consts bind :: "['a maybe, 'a => 'b maybe] => 'b maybe" (infixl 60)
+consts bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
defs
bind_def "m bind f == case m of Ok r => f r | Fail => Fail"
--- a/src/HOL/MiniML/MiniML.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/MiniML/MiniML.thy Fri Dec 01 12:03:13 1995 +0100
@@ -16,7 +16,7 @@
consts
has_type :: "(type_expr list * expr * type_expr)set"
syntax
- "@has_type" :: "[type_expr list, expr, type_expr] => bool"
+ "@has_type" :: [type_expr list, expr, type_expr] => bool
("((_) |-/ (_) :: (_))" 60)
translations
"a |- e :: t" == "(a,e,t):has_type"
--- a/src/HOL/MiniML/Type.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/MiniML/Type.thy Fri Dec 01 12:03:13 1995 +0100
@@ -29,13 +29,13 @@
(* identity *)
consts
- id_subst :: "subst"
+ id_subst :: subst
defs
id_subst_def "id_subst == (%n.TVar n)"
(* extension of substitution to type structures *)
consts
- app_subst :: "[subst, 'a::type_struct] => 'a::type_struct" ("$")
+ app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
rules
app_subst_TVar "$ s (TVar n) = s n"
@@ -45,7 +45,7 @@
(* free_tv s: the type variables occuring freely in the type structure s *)
consts
- free_tv :: "['a::type_struct] => nat set"
+ free_tv :: ['a::type_struct] => nat set
rules
free_tv_TVar "free_tv (TVar m) = {m}"
@@ -55,13 +55,13 @@
(* domain of a substitution *)
consts
- dom :: "subst => nat set"
+ dom :: subst => nat set
defs
dom_def "dom s == {n. s n ~= TVar n}"
(* codomain of a substitutions: the introduced variables *)
consts
- cod :: "subst => nat set"
+ cod :: subst => nat set
defs
cod_def "cod s == (UN m:dom s. free_tv (s m))"
@@ -72,13 +72,13 @@
structure s, i.e. whether n is greater than any type variable
occuring in the type structure *)
consts
- new_tv :: "[nat,'a::type_struct] => bool"
+ new_tv :: [nat,'a::type_struct] => bool
defs
new_tv_def "new_tv n ts == ! m. m:free_tv ts --> m<n"
(* unification algorithm mgu *)
consts
- mgu :: "[type_expr,type_expr] => subst maybe"
+ mgu :: [type_expr,type_expr] => subst maybe
rules
mgu_eq "mgu t1 t2 = Ok u ==> $ u t1 = $ u t2"
mgu_mg "[| (mgu t1 t2) = Ok u; $ s t1 = $ s t2 |] ==>
--- a/src/HOL/MiniML/W.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/MiniML/W.thy Fri Dec 01 12:03:13 1995 +0100
@@ -13,7 +13,7 @@
(* type inference algorithm W *)
consts
- W :: "[expr, type_expr list, nat] => result_W"
+ W :: [expr, type_expr list, nat] => result_W
primrec W expr
W_Var "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
--- a/src/HOL/ex/BT.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/BT.thy Fri Dec 01 12:03:13 1995 +0100
@@ -11,13 +11,13 @@
datatype 'a bt = Lf | Br 'a ('a bt) ('a bt)
consts
- n_nodes :: "'a bt => nat"
- n_leaves :: "'a bt => nat"
- reflect :: "'a bt => 'a bt"
- bt_map :: "('a=>'b) => ('a bt => 'b bt)"
- preorder :: "'a bt => 'a list"
- inorder :: "'a bt => 'a list"
- postorder :: "'a bt => 'a list"
+ n_nodes :: 'a bt => nat
+ n_leaves :: 'a bt => nat
+ reflect :: 'a bt => 'a bt
+ bt_map :: ('a=>'b) => ('a bt => 'b bt)
+ preorder :: 'a bt => 'a list
+ inorder :: 'a bt => 'a list
+ postorder :: 'a bt => 'a list
primrec n_nodes bt
n_nodes_Lf "n_nodes (Lf) = 0"
--- a/src/HOL/ex/InSort.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/InSort.thy Fri Dec 01 12:03:13 1995 +0100
@@ -9,8 +9,8 @@
InSort = Sorting +
consts
- ins :: "[['a,'a]=>bool, 'a, 'a list] => 'a list"
- insort :: "[['a,'a]=>bool, 'a list] => 'a list"
+ ins :: [['a,'a]=>bool, 'a, 'a list] => 'a list
+ insort :: [['a,'a]=>bool, 'a list] => 'a list
primrec ins List.list
ins_Nil "ins f x [] = [x]"
--- a/src/HOL/ex/LList.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/LList.thy Fri Dec 01 12:03:13 1995 +0100
@@ -32,34 +32,34 @@
llist :: (term)term
consts
- list_Fun :: "['a item set, 'a item set] => 'a item set"
+ list_Fun :: ['a item set, 'a item set] => 'a item set
LListD_Fun ::
"[('a item * 'a item)set, ('a item * 'a item)set] =>
('a item * 'a item)set"
- llist :: "'a item set => 'a item set"
+ llist :: 'a item set => 'a item set
LListD :: "('a item * 'a item)set => ('a item * 'a item)set"
llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
- Rep_llist :: "'a llist => 'a item"
- Abs_llist :: "'a item => 'a llist"
- LNil :: "'a llist"
- LCons :: "['a, 'a llist] => 'a llist"
+ Rep_llist :: 'a llist => 'a item
+ Abs_llist :: 'a item => 'a llist
+ LNil :: 'a llist
+ LCons :: ['a, 'a llist] => 'a llist
- llist_case :: "['b, ['a, 'a llist]=>'b, 'a llist] => 'b"
+ llist_case :: ['b, ['a, 'a llist]=>'b, 'a llist] => 'b
LList_corec_fun :: "[nat, 'a=>unit+('b item * 'a), 'a] => 'b item"
LList_corec :: "['a, 'a => unit + ('b item * 'a)] => 'b item"
llist_corec :: "['a, 'a => unit + ('b * 'a)] => 'b llist"
- Lmap :: "('a item => 'b item) => ('a item => 'b item)"
- lmap :: "('a=>'b) => ('a llist => 'b llist)"
+ Lmap :: ('a item => 'b item) => ('a item => 'b item)
+ lmap :: ('a=>'b) => ('a llist => 'b llist)
- iterates :: "['a => 'a, 'a] => 'a llist"
+ iterates :: ['a => 'a, 'a] => 'a llist
- Lconst :: "'a item => 'a item"
- Lappend :: "['a item, 'a item] => 'a item"
- lappend :: "['a llist, 'a llist] => 'a llist"
+ Lconst :: 'a item => 'a item
+ Lappend :: ['a item, 'a item] => 'a item
+ lappend :: ['a llist, 'a llist] => 'a llist
coinductive "llist(A)"
--- a/src/HOL/ex/MT.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/MT.thy Fri Dec 01 12:03:13 1995 +0100
@@ -46,48 +46,48 @@
TyEnv :: term
consts
- c_app :: "[Const, Const] => Const"
+ c_app :: [Const, Const] => Const
- e_const :: "Const => Ex"
- e_var :: "ExVar => Ex"
- e_fn :: "[ExVar, Ex] => Ex" ("fn _ => _" [0,51] 1000)
- e_fix :: "[ExVar, ExVar, Ex] => Ex" ("fix _ ( _ ) = _" [0,51,51] 1000)
- e_app :: "[Ex, Ex] => Ex" ("_ @ _" [51,51] 1000)
- e_const_fst :: "Ex => Const"
+ e_const :: Const => Ex
+ e_var :: ExVar => Ex
+ e_fn :: [ExVar, Ex] => Ex ("fn _ => _" [0,51] 1000)
+ e_fix :: [ExVar, ExVar, Ex] => Ex ("fix _ ( _ ) = _" [0,51,51] 1000)
+ e_app :: [Ex, Ex] => Ex ("_ @ _" [51,51] 1000)
+ e_const_fst :: Ex => Const
- t_const :: "TyConst => Ty"
- t_fun :: "[Ty, Ty] => Ty" ("_ -> _" [51,51] 1000)
+ t_const :: TyConst => Ty
+ t_fun :: [Ty, Ty] => Ty ("_ -> _" [51,51] 1000)
- v_const :: "Const => Val"
- v_clos :: "Clos => Val"
+ v_const :: Const => Val
+ v_clos :: Clos => Val
- ve_emp :: "ValEnv"
- ve_owr :: "[ValEnv, ExVar, Val] => ValEnv" ("_ + { _ |-> _ }" [36,0,0] 50)
- ve_dom :: "ValEnv => ExVar set"
- ve_app :: "[ValEnv, ExVar] => Val"
+ ve_emp :: ValEnv
+ ve_owr :: [ValEnv, ExVar, Val] => ValEnv ("_ + { _ |-> _ }" [36,0,0] 50)
+ ve_dom :: ValEnv => ExVar set
+ ve_app :: [ValEnv, ExVar] => Val
- clos_mk :: "[ExVar, Ex, ValEnv] => Clos" ("<| _ , _ , _ |>" [0,0,0] 1000)
+ clos_mk :: [ExVar, Ex, ValEnv] => Clos ("<| _ , _ , _ |>" [0,0,0] 1000)
- te_emp :: "TyEnv"
- te_owr :: "[TyEnv, ExVar, Ty] => TyEnv" ("_ + { _ |=> _ }" [36,0,0] 50)
- te_app :: "[TyEnv, ExVar] => Ty"
- te_dom :: "TyEnv => ExVar set"
+ te_emp :: TyEnv
+ te_owr :: [TyEnv, ExVar, Ty] => TyEnv ("_ + { _ |=> _ }" [36,0,0] 50)
+ te_app :: [TyEnv, ExVar] => Ty
+ te_dom :: TyEnv => ExVar set
eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set"
eval_rel :: "((ValEnv * Ex) * Val) set"
- eval :: "[ValEnv, Ex, Val] => bool" ("_ |- _ ---> _" [36,0,36] 50)
+ eval :: [ValEnv, Ex, Val] => bool ("_ |- _ ---> _" [36,0,36] 50)
elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set"
elab_rel :: "((TyEnv * Ex) * Ty) set"
- elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50)
+ elab :: [TyEnv, Ex, Ty] => bool ("_ |- _ ===> _" [36,0,36] 50)
- isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50)
- isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _")
+ isof :: [Const, Ty] => bool ("_ isof _" [36,36] 50)
+ isof_env :: [ValEnv,TyEnv] => bool ("_ isofenv _")
hasty_fun :: "(Val * Ty) set => (Val * Ty) set"
hasty_rel :: "(Val * Ty) set"
- hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50)
- hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35)
+ hasty :: [Val, Ty] => bool ("_ hasty _" [36,36] 50)
+ hasty_env :: [ValEnv,TyEnv] => bool ("_ hastyenv _ " [36,36] 35)
rules
--- a/src/HOL/ex/NatSum.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/NatSum.thy Fri Dec 01 12:03:13 1995 +0100
@@ -7,7 +7,7 @@
*)
NatSum = Arith +
-consts sum :: "[nat=>nat, nat] => nat"
+consts sum :: [nat=>nat, nat] => nat
rules sum_0 "sum f 0 = 0"
sum_Suc "sum f (Suc n) = f(n) + sum f n"
end
--- a/src/HOL/ex/Perm.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/Perm.thy Fri Dec 01 12:03:13 1995 +0100
@@ -9,7 +9,7 @@
Perm = List +
consts perm :: "('a list * 'a list) set"
-syntax "@perm" :: "['a list, 'a list] => bool" ("_ <~~> _" [50,50] 50)
+syntax "@perm" :: ['a list, 'a list] => bool ("_ <~~> _" [50,50] 50)
translations
"x <~~> y" == "(x,y) : perm"
--- a/src/HOL/ex/PropLog.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/PropLog.thy Fri Dec 01 12:03:13 1995 +0100
@@ -10,12 +10,12 @@
datatype
'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
consts
- thms :: "'a pl set => 'a pl set"
- "|-" :: "['a pl set, 'a pl] => bool" (infixl 50)
- "|=" :: "['a pl set, 'a pl] => bool" (infixl 50)
- eval2 :: "['a pl, 'a set] => bool"
- eval :: "['a set, 'a pl] => bool" ("_[_]" [100,0] 100)
- hyps :: "['a pl, 'a set] => 'a pl set"
+ thms :: 'a pl set => 'a pl set
+ "|-" :: ['a pl set, 'a pl] => bool (infixl 50)
+ "|=" :: ['a pl set, 'a pl] => bool (infixl 50)
+ eval2 :: ['a pl, 'a set] => bool
+ eval :: ['a set, 'a pl] => bool ("_[_]" [100,0] 100)
+ hyps :: ['a pl, 'a set] => 'a pl set
translations
"H |- p" == "p : thms(H)"
--- a/src/HOL/ex/Puzzle.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/Puzzle.thy Fri Dec 01 12:03:13 1995 +0100
@@ -7,6 +7,6 @@
*)
Puzzle = Nat +
-consts f :: "nat => nat"
+consts f :: nat => nat
rules f_ax "f(f(n)) < f(Suc(n))"
end
--- a/src/HOL/ex/Qsort.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/Qsort.thy Fri Dec 01 12:03:13 1995 +0100
@@ -8,7 +8,7 @@
Qsort = Sorting +
consts
- qsort :: "[['a,'a] => bool, 'a list] => 'a list"
+ qsort :: [['a,'a] => bool, 'a list] => 'a list
rules
--- a/src/HOL/ex/Rec.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/Rec.thy Fri Dec 01 12:03:13 1995 +0100
@@ -1,8 +1,8 @@
Rec = Fixedpt +
consts
-fix :: "('a=>'a) => 'a"
-Dom :: "(('a=>'b) => ('a=>'b)) => 'a set"
-Domf :: "(('a=>'b) => ('a=>'b)) => 'a set => 'a set"
+fix :: ('a=>'a) => 'a
+Dom :: (('a=>'b) => ('a=>'b)) => 'a set
+Domf :: (('a=>'b) => ('a=>'b)) => 'a set => 'a set
rules
Domf_def "Domf(F,D) == {y . !f g. (!x:D. f(x)=g(x)) --> F(f,y)=F(g,y)}"
Dom_def "Dom(F) == lfp(Domf(F))"
--- a/src/HOL/ex/SList.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/SList.thy Fri Dec 01 12:03:13 1995 +0100
@@ -21,36 +21,36 @@
consts
- list :: "'a item set => 'a item set"
- Rep_list :: "'a list => 'a item"
- Abs_list :: "'a item => 'a list"
- NIL :: "'a item"
- CONS :: "['a item, 'a item] => 'a item"
- Nil :: "'a list"
- "#" :: "['a, 'a list] => 'a list" (infixr 65)
- List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b"
- List_rec :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b"
- list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
- list_rec :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
- Rep_map :: "('b => 'a item) => ('b list => 'a item)"
- Abs_map :: "('a item => 'b) => 'a item => 'b list"
- null :: "'a list => bool"
- hd :: "'a list => 'a"
- tl,ttl :: "'a list => 'a list"
- mem :: "['a, 'a list] => bool" (infixl 55)
- list_all :: "('a => bool) => ('a list => bool)"
- map :: "('a=>'b) => ('a list => 'b list)"
- "@" :: "['a list, 'a list] => 'a list" (infixr 65)
- filter :: "['a => bool, 'a list] => 'a list"
+ list :: 'a item set => 'a item set
+ Rep_list :: 'a list => 'a item
+ Abs_list :: 'a item => 'a list
+ NIL :: 'a item
+ CONS :: ['a item, 'a item] => 'a item
+ Nil :: 'a list
+ "#" :: ['a, 'a list] => 'a list (infixr 65)
+ List_case :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
+ List_rec :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
+ list_case :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
+ list_rec :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
+ Rep_map :: ('b => 'a item) => ('b list => 'a item)
+ Abs_map :: ('a item => 'b) => 'a item => 'b list
+ null :: 'a list => bool
+ hd :: 'a list => 'a
+ tl,ttl :: 'a list => 'a list
+ mem :: ['a, 'a list] => bool (infixl 55)
+ list_all :: ('a => bool) => ('a list => bool)
+ map :: ('a=>'b) => ('a list => 'b list)
+ "@" :: ['a list, 'a list] => 'a list (infixr 65)
+ filter :: ['a => bool, 'a list] => 'a list
(* list Enumeration *)
- "[]" :: "'a list" ("[]")
- "@list" :: "args => 'a list" ("[(_)]")
+ "[]" :: 'a list ("[]")
+ "@list" :: args => 'a list ("[(_)]")
(* Special syntax for list_all and filter *)
- "@Alls" :: "[idt, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10)
- "@filter" :: "[idt, 'a list, bool] => 'a list" ("(1[_:_ ./ _])")
+ "@Alls" :: [idt, 'a list, bool] => bool ("(2Alls _:_./ _)" 10)
+ "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
translations
"[x, xs]" == "x#[xs]"
--- a/src/HOL/ex/Simult.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/Simult.thy Fri Dec 01 12:03:13 1995 +0100
@@ -21,16 +21,16 @@
arities tree,forest :: (term)term
consts
- TF :: "'a item set => 'a item set"
- FNIL :: "'a item"
- TCONS,FCONS :: "['a item, 'a item] => 'a item"
- Rep_Tree :: "'a tree => 'a item"
- Abs_Tree :: "'a item => 'a tree"
- Rep_Forest :: "'a forest => 'a item"
- Abs_Forest :: "'a item => 'a forest"
- Tcons :: "['a, 'a forest] => 'a tree"
- Fcons :: "['a tree, 'a forest] => 'a forest"
- Fnil :: "'a forest"
+ TF :: 'a item set => 'a item set
+ FNIL :: 'a item
+ TCONS,FCONS :: ['a item, 'a item] => 'a item
+ Rep_Tree :: 'a tree => 'a item
+ Abs_Tree :: 'a item => 'a tree
+ Rep_Forest :: 'a forest => 'a item
+ Abs_Forest :: 'a item => 'a forest
+ Tcons :: ['a, 'a forest] => 'a tree
+ Fcons :: ['a tree, 'a forest] => 'a forest
+ Fnil :: 'a forest
TF_rec :: "['a item, ['a item , 'a item, 'b]=>'b,
'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b"
tree_rec :: "['a tree, ['a, 'a forest, 'b]=>'b,
--- a/src/HOL/ex/Sorting.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/Sorting.thy Fri Dec 01 12:03:13 1995 +0100
@@ -8,11 +8,11 @@
Sorting = List +
consts
- sorted1:: "[['a,'a] => bool, 'a list] => bool"
- sorted :: "[['a,'a] => bool, 'a list] => bool"
- mset :: "'a list => ('a => nat)"
- total :: "(['a,'a] => bool) => bool"
- transf :: "(['a,'a] => bool) => bool"
+ sorted1:: [['a,'a] => bool, 'a list] => bool
+ sorted :: [['a,'a] => bool, 'a list] => bool
+ mset :: 'a list => ('a => nat)
+ total :: (['a,'a] => bool) => bool
+ transf :: (['a,'a] => bool) => bool
rules
--- a/src/HOL/ex/String.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/String.thy Fri Dec 01 12:03:13 1995 +0100
@@ -17,8 +17,8 @@
string = "char list"
syntax
- "_Char" :: "xstr => char" ("CHR _")
- "_String" :: "xstr => string" ("_")
+ "_Char" :: xstr => char ("CHR _")
+ "_String" :: xstr => string ("_")
end
--- a/src/HOL/ex/Term.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/Term.thy Fri Dec 01 12:03:13 1995 +0100
@@ -16,14 +16,14 @@
arities term :: (term)term
consts
- term :: "'a item set => 'a item set"
- Rep_term :: "'a term => 'a item"
- Abs_term :: "'a item => 'a term"
- Rep_Tlist :: "'a term list => 'a item"
- Abs_Tlist :: "'a item => 'a term list"
- App :: "['a, ('a term)list] => 'a term"
- Term_rec :: "['a item, ['a item , 'a item, 'b list]=>'b] => 'b"
- term_rec :: "['a term, ['a ,'a term list, 'b list]=>'b] => 'b"
+ term :: 'a item set => 'a item set
+ Rep_term :: 'a term => 'a item
+ Abs_term :: 'a item => 'a term
+ Rep_Tlist :: 'a term list => 'a item
+ Abs_Tlist :: 'a item => 'a term list
+ App :: ['a, ('a term)list] => 'a term
+ Term_rec :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
+ term_rec :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
inductive "term(A)"
intrs