removed quotes from consts and syntax sections
authorclasohm
Fri Dec 01 12:03:13 1995 +0100 (1995-12-01)
changeset 137692f83b9d17e1
parent 1375 d04af07266e8
child 1377 f800f533aa83
removed quotes from consts and syntax sections
src/HOL/IOA/ABP/Abschannel.thy
src/HOL/IOA/ABP/Abschannel_finite.thy
src/HOL/IOA/ABP/Correctness.thy
src/HOL/IOA/ABP/Env.thy
src/HOL/IOA/ABP/Impl.thy
src/HOL/IOA/ABP/Impl_finite.thy
src/HOL/IOA/ABP/Packet.thy
src/HOL/IOA/ABP/Receiver.thy
src/HOL/IOA/ABP/Sender.thy
src/HOL/IOA/ABP/Spec.thy
src/HOL/IOA/NTP/Abschannel.thy
src/HOL/IOA/NTP/Correctness.thy
src/HOL/IOA/NTP/Impl.thy
src/HOL/IOA/NTP/Multiset.thy
src/HOL/IOA/NTP/Packet.thy
src/HOL/IOA/NTP/Receiver.thy
src/HOL/IOA/NTP/Sender.thy
src/HOL/IOA/NTP/Spec.thy
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/ParRed.thy
src/HOL/MiniML/I.thy
src/HOL/MiniML/Maybe.thy
src/HOL/MiniML/MiniML.thy
src/HOL/MiniML/Type.thy
src/HOL/MiniML/W.thy
src/HOL/ex/BT.thy
src/HOL/ex/InSort.thy
src/HOL/ex/LList.thy
src/HOL/ex/MT.thy
src/HOL/ex/NatSum.thy
src/HOL/ex/Perm.thy
src/HOL/ex/PropLog.thy
src/HOL/ex/Puzzle.thy
src/HOL/ex/Qsort.thy
src/HOL/ex/Rec.thy
src/HOL/ex/SList.thy
src/HOL/ex/Simult.thy
src/HOL/ex/Sorting.thy
src/HOL/ex/String.thy
src/HOL/ex/Term.thy
     1.1 --- a/src/HOL/IOA/ABP/Abschannel.thy	Thu Nov 30 12:58:44 1995 +0100
     1.2 +++ b/src/HOL/IOA/ABP/Abschannel.thy	Fri Dec 01 12:03:13 1995 +0100
     1.3 @@ -14,21 +14,21 @@
     1.4  
     1.5  consts
     1.6   
     1.7 -ch_asig  :: "'a act signature"
     1.8 -ch_trans :: "('a act, 'a list)transition set"
     1.9 -ch_ioa   :: "('a act, 'a list)ioa"
    1.10 +ch_asig  :: 'a act signature
    1.11 +ch_trans :: ('a act, 'a list)transition set
    1.12 +ch_ioa   :: ('a act, 'a list)ioa
    1.13  
    1.14 -rsch_actions  :: "'m action => bool act option"
    1.15 +rsch_actions  :: 'm action => bool act option
    1.16  srch_actions  :: "'m action =>(bool * 'm) act option"
    1.17  
    1.18  srch_asig, 
    1.19 -rsch_asig  :: "'m action signature"
    1.20 +rsch_asig  :: 'm action signature
    1.21  
    1.22 -srch_trans :: "('m action, 'm packet list)transition set"
    1.23 -rsch_trans :: "('m action, bool list)transition set"
    1.24 +srch_trans :: ('m action, 'm packet list)transition set
    1.25 +rsch_trans :: ('m action, bool list)transition set
    1.26  
    1.27 -srch_ioa   :: "('m action, 'm packet list)ioa"
    1.28 -rsch_ioa   :: "('m action, bool list)ioa"   
    1.29 +srch_ioa   :: ('m action, 'm packet list)ioa
    1.30 +rsch_ioa   :: ('m action, bool list)ioa   
    1.31  
    1.32  
    1.33  defs
     2.1 --- a/src/HOL/IOA/ABP/Abschannel_finite.thy	Thu Nov 30 12:58:44 1995 +0100
     2.2 +++ b/src/HOL/IOA/ABP/Abschannel_finite.thy	Fri Dec 01 12:03:13 1995 +0100
     2.3 @@ -10,22 +10,22 @@
     2.4   
     2.5  consts
     2.6   
     2.7 -ch_fin_asig  :: "'a act signature"
     2.8 +ch_fin_asig  :: 'a act signature
     2.9  
    2.10 -ch_fin_trans :: "('a act, 'a list)transition set"
    2.11 +ch_fin_trans :: ('a act, 'a list)transition set
    2.12  
    2.13 -ch_fin_ioa   :: "('a act, 'a list)ioa"
    2.14 +ch_fin_ioa   :: ('a act, 'a list)ioa
    2.15  
    2.16  srch_fin_asig, 
    2.17 -rsch_fin_asig  :: "'m action signature"
    2.18 +rsch_fin_asig  :: 'm action signature
    2.19  
    2.20 -srch_fin_trans :: "('m action, 'm packet list)transition set"
    2.21 -rsch_fin_trans :: "('m action, bool list)transition set"
    2.22 +srch_fin_trans :: ('m action, 'm packet list)transition set
    2.23 +rsch_fin_trans :: ('m action, bool list)transition set
    2.24  
    2.25 -srch_fin_ioa   :: "('m action, 'm packet list)ioa"
    2.26 -rsch_fin_ioa   :: "('m action, bool list)ioa"   
    2.27 +srch_fin_ioa   :: ('m action, 'm packet list)ioa
    2.28 +rsch_fin_ioa   :: ('m action, bool list)ioa   
    2.29  
    2.30 -reverse        :: "'a list => 'a list"
    2.31 +reverse        :: 'a list => 'a list
    2.32  
    2.33  primrec
    2.34    reverse List.list  
     3.1 --- a/src/HOL/IOA/ABP/Correctness.thy	Thu Nov 30 12:58:44 1995 +0100
     3.2 +++ b/src/HOL/IOA/ABP/Correctness.thy	Fri Dec 01 12:03:13 1995 +0100
     3.3 @@ -10,9 +10,9 @@
     3.4  
     3.5  consts
     3.6  
     3.7 -reduce           :: "'a list => 'a list"
     3.8 +reduce           :: 'a list => 'a list
     3.9  
    3.10 -abs              :: "'c"
    3.11 +abs              :: 'c
    3.12  system_ioa       :: "('m action, bool * 'm impl_state)ioa"
    3.13  system_fin_ioa   :: "('m action, bool * 'm impl_state)ioa"
    3.14    
     4.1 --- a/src/HOL/IOA/ABP/Env.thy	Thu Nov 30 12:58:44 1995 +0100
     4.2 +++ b/src/HOL/IOA/ABP/Env.thy	Fri Dec 01 12:03:13 1995 +0100
     4.3 @@ -16,10 +16,10 @@
     4.4  
     4.5  consts
     4.6  
     4.7 -env_asig   :: "'m action signature"
     4.8 -env_trans  :: "('m action, 'm env_state)transition set"
     4.9 -env_ioa    :: "('m action, 'm env_state)ioa"
    4.10 -next       :: "'m env_state => bool"
    4.11 +env_asig   :: 'm action signature
    4.12 +env_trans  :: ('m action, 'm env_state)transition set
    4.13 +env_ioa    :: ('m action, 'm env_state)ioa
    4.14 +next       :: 'm env_state => bool
    4.15  
    4.16  defs
    4.17  
     5.1 --- a/src/HOL/IOA/ABP/Impl.thy	Thu Nov 30 12:58:44 1995 +0100
     5.2 +++ b/src/HOL/IOA/ABP/Impl.thy	Fri Dec 01 12:03:13 1995 +0100
     5.3 @@ -16,11 +16,11 @@
     5.4  
     5.5  
     5.6  consts
     5.7 - impl_ioa    :: "('m action, 'm impl_state)ioa"
     5.8 - sen         :: "'m impl_state => 'm sender_state"
     5.9 - rec         :: "'m impl_state => 'm receiver_state"
    5.10 - srch        :: "'m impl_state => 'm packet list"
    5.11 - rsch        :: "'m impl_state => bool list"
    5.12 + impl_ioa    :: ('m action, 'm impl_state)ioa
    5.13 + sen         :: 'm impl_state => 'm sender_state
    5.14 + rec         :: 'm impl_state => 'm receiver_state
    5.15 + srch        :: 'm impl_state => 'm packet list
    5.16 + rsch        :: 'm impl_state => bool list
    5.17  
    5.18  defs
    5.19  
     6.1 --- a/src/HOL/IOA/ABP/Impl_finite.thy	Thu Nov 30 12:58:44 1995 +0100
     6.2 +++ b/src/HOL/IOA/ABP/Impl_finite.thy	Fri Dec 01 12:03:13 1995 +0100
     6.3 @@ -16,11 +16,11 @@
     6.4  
     6.5  consts
     6.6  
     6.7 - impl_fin_ioa    :: "('m action, 'm impl_fin_state)ioa"
     6.8 - sen_fin         :: "'m impl_fin_state => 'm sender_state"
     6.9 - rec_fin         :: "'m impl_fin_state => 'm receiver_state"
    6.10 - srch_fin        :: "'m impl_fin_state => 'm packet list"
    6.11 - rsch_fin        :: "'m impl_fin_state => bool list"
    6.12 + impl_fin_ioa    :: ('m action, 'm impl_fin_state)ioa
    6.13 + sen_fin         :: 'm impl_fin_state => 'm sender_state
    6.14 + rec_fin         :: 'm impl_fin_state => 'm receiver_state
    6.15 + srch_fin        :: 'm impl_fin_state => 'm packet list
    6.16 + rsch_fin        :: 'm impl_fin_state => bool list
    6.17  
    6.18  defs
    6.19  
     7.1 --- a/src/HOL/IOA/ABP/Packet.thy	Thu Nov 30 12:58:44 1995 +0100
     7.2 +++ b/src/HOL/IOA/ABP/Packet.thy	Fri Dec 01 12:03:13 1995 +0100
     7.3 @@ -14,8 +14,8 @@
     7.4  
     7.5  consts
     7.6  
     7.7 -  hdr  :: "'msg packet => bool"
     7.8 -  msg :: "'msg packet => 'msg"
     7.9 +  hdr  :: 'msg packet => bool
    7.10 +  msg :: 'msg packet => 'msg
    7.11  
    7.12  defs
    7.13  
     8.1 --- a/src/HOL/IOA/ABP/Receiver.thy	Thu Nov 30 12:58:44 1995 +0100
     8.2 +++ b/src/HOL/IOA/ABP/Receiver.thy	Fri Dec 01 12:03:13 1995 +0100
     8.3 @@ -16,11 +16,11 @@
     8.4  
     8.5  consts
     8.6  
     8.7 -  receiver_asig :: "'m action signature"
     8.8 -  receiver_trans:: "('m action, 'm receiver_state)transition set"
     8.9 -  receiver_ioa  :: "('m action, 'm receiver_state)ioa"
    8.10 -  rq            :: "'m receiver_state => 'm list"
    8.11 -  rbit          :: "'m receiver_state => bool"
    8.12 +  receiver_asig :: 'm action signature
    8.13 +  receiver_trans:: ('m action, 'm receiver_state)transition set
    8.14 +  receiver_ioa  :: ('m action, 'm receiver_state)ioa
    8.15 +  rq            :: 'm receiver_state => 'm list
    8.16 +  rbit          :: 'm receiver_state => bool
    8.17  
    8.18  defs
    8.19  
     9.1 --- a/src/HOL/IOA/ABP/Sender.thy	Thu Nov 30 12:58:44 1995 +0100
     9.2 +++ b/src/HOL/IOA/ABP/Sender.thy	Fri Dec 01 12:03:13 1995 +0100
     9.3 @@ -15,11 +15,11 @@
     9.4  
     9.5  consts
     9.6  
     9.7 -sender_asig   :: "'m action signature"
     9.8 -sender_trans  :: "('m action, 'm sender_state)transition set"
     9.9 -sender_ioa    :: "('m action, 'm sender_state)ioa"
    9.10 -sq            :: "'m sender_state => 'm list"
    9.11 -sbit          :: "'m sender_state => bool"
    9.12 +sender_asig   :: 'm action signature
    9.13 +sender_trans  :: ('m action, 'm sender_state)transition set
    9.14 +sender_ioa    :: ('m action, 'm sender_state)ioa
    9.15 +sq            :: 'm sender_state => 'm list
    9.16 +sbit          :: 'm sender_state => bool
    9.17  
    9.18  defs
    9.19  
    10.1 --- a/src/HOL/IOA/ABP/Spec.thy	Thu Nov 30 12:58:44 1995 +0100
    10.2 +++ b/src/HOL/IOA/ABP/Spec.thy	Fri Dec 01 12:03:13 1995 +0100
    10.3 @@ -10,9 +10,9 @@
    10.4  
    10.5  consts
    10.6  
    10.7 -spec_sig   :: "'m action signature"
    10.8 -spec_trans :: "('m action, 'm list)transition set"
    10.9 -spec_ioa   :: "('m action, 'm list)ioa"
   10.10 +spec_sig   :: 'm action signature
   10.11 +spec_trans :: ('m action, 'm list)transition set
   10.12 +spec_ioa   :: ('m action, 'm list)ioa
   10.13  
   10.14  defs
   10.15  
    11.1 --- a/src/HOL/IOA/NTP/Abschannel.thy	Thu Nov 30 12:58:44 1995 +0100
    11.2 +++ b/src/HOL/IOA/NTP/Abschannel.thy	Fri Dec 01 12:03:13 1995 +0100
    11.3 @@ -12,23 +12,23 @@
    11.4  
    11.5  consts
    11.6   
    11.7 -ch_asig  :: "'a act signature"
    11.8 +ch_asig  :: 'a act signature
    11.9  
   11.10 -ch_trans :: "('a act, 'a multiset)transition set"
   11.11 +ch_trans :: ('a act, 'a multiset)transition set
   11.12  
   11.13 -ch_ioa   :: "('a act, 'a multiset)ioa"
   11.14 +ch_ioa   :: ('a act, 'a multiset)ioa
   11.15  
   11.16 -rsch_actions  :: "'m action => bool act option"
   11.17 +rsch_actions  :: 'm action => bool act option
   11.18  srch_actions  :: "'m action =>(bool * 'm) act option"
   11.19  
   11.20  srch_asig, 
   11.21 -rsch_asig  :: "'m action signature"
   11.22 +rsch_asig  :: 'm action signature
   11.23  
   11.24 -srch_trans :: "('m action, 'm packet multiset)transition set"
   11.25 -rsch_trans :: "('m action, bool multiset)transition set"
   11.26 +srch_trans :: ('m action, 'm packet multiset)transition set
   11.27 +rsch_trans :: ('m action, bool multiset)transition set
   11.28  
   11.29 -srch_ioa   :: "('m action, 'm packet multiset)ioa"
   11.30 -rsch_ioa   :: "('m action, bool multiset)ioa"   
   11.31 +srch_ioa   :: ('m action, 'm packet multiset)ioa
   11.32 +rsch_ioa   :: ('m action, bool multiset)ioa   
   11.33  
   11.34  
   11.35  defs
    12.1 --- a/src/HOL/IOA/NTP/Correctness.thy	Thu Nov 30 12:58:44 1995 +0100
    12.2 +++ b/src/HOL/IOA/NTP/Correctness.thy	Fri Dec 01 12:03:13 1995 +0100
    12.3 @@ -10,7 +10,7 @@
    12.4  
    12.5  consts
    12.6  
    12.7 -hom :: "'m impl_state => 'm list"
    12.8 +hom :: 'm impl_state => 'm list
    12.9  
   12.10  defs
   12.11  
    13.1 --- a/src/HOL/IOA/NTP/Impl.thy	Thu Nov 30 12:58:44 1995 +0100
    13.2 +++ b/src/HOL/IOA/NTP/Impl.thy	Fri Dec 01 12:03:13 1995 +0100
    13.3 @@ -16,14 +16,14 @@
    13.4  
    13.5  
    13.6  consts
    13.7 - impl_ioa    :: "('m action, 'm impl_state)ioa"
    13.8 - sen         :: "'m impl_state => 'm sender_state"
    13.9 - rec         :: "'m impl_state => 'm receiver_state"
   13.10 - srch        :: "'m impl_state => 'm packet multiset"
   13.11 - rsch        :: "'m impl_state => bool multiset"
   13.12 + impl_ioa    :: ('m action, 'm impl_state)ioa
   13.13 + sen         :: 'm impl_state => 'm sender_state
   13.14 + rec         :: 'm impl_state => 'm receiver_state
   13.15 + srch        :: 'm impl_state => 'm packet multiset
   13.16 + rsch        :: 'm impl_state => bool multiset
   13.17   inv1, inv2, 
   13.18 - inv3, inv4  :: "'m impl_state => bool"
   13.19 - hdr_sum     :: "'m packet multiset => bool => nat"
   13.20 + inv3, inv4  :: 'm impl_state => bool
   13.21 + hdr_sum     :: 'm packet multiset => bool => nat
   13.22  
   13.23  defs
   13.24  
    14.1 --- a/src/HOL/IOA/NTP/Multiset.thy	Thu Nov 30 12:58:44 1995 +0100
    14.2 +++ b/src/HOL/IOA/NTP/Multiset.thy	Fri Dec 01 12:03:13 1995 +0100
    14.3 @@ -19,11 +19,11 @@
    14.4  
    14.5  consts
    14.6  
    14.7 -  "{|}"  :: "'a multiset"                        ("{|}")
    14.8 -  addm   :: "['a multiset, 'a] => 'a multiset"
    14.9 -  delm   :: "['a multiset, 'a] => 'a multiset"
   14.10 -  countm :: "['a multiset, 'a => bool] => nat"
   14.11 -  count  :: "['a multiset, 'a] => nat"
   14.12 +  "{|}"  :: 'a multiset                        ("{|}")
   14.13 +  addm   :: ['a multiset, 'a] => 'a multiset
   14.14 +  delm   :: ['a multiset, 'a] => 'a multiset
   14.15 +  countm :: ['a multiset, 'a => bool] => nat
   14.16 +  count  :: ['a multiset, 'a] => nat
   14.17  
   14.18  rules
   14.19  
    15.1 --- a/src/HOL/IOA/NTP/Packet.thy	Thu Nov 30 12:58:44 1995 +0100
    15.2 +++ b/src/HOL/IOA/NTP/Packet.thy	Fri Dec 01 12:03:13 1995 +0100
    15.3 @@ -14,8 +14,8 @@
    15.4  
    15.5  consts
    15.6  
    15.7 -  hdr  :: "'msg packet => bool"
    15.8 -  msg :: "'msg packet => 'msg"
    15.9 +  hdr  :: 'msg packet => bool
   15.10 +  msg :: 'msg packet => 'msg
   15.11  
   15.12  defs
   15.13  
    16.1 --- a/src/HOL/IOA/NTP/Receiver.thy	Thu Nov 30 12:58:44 1995 +0100
    16.2 +++ b/src/HOL/IOA/NTP/Receiver.thy	Fri Dec 01 12:03:13 1995 +0100
    16.3 @@ -16,14 +16,14 @@
    16.4  
    16.5  consts
    16.6  
    16.7 -  receiver_asig :: "'m action signature"
    16.8 -  receiver_trans:: "('m action, 'm receiver_state)transition set"
    16.9 -  receiver_ioa  :: "('m action, 'm receiver_state)ioa"
   16.10 -  rq            :: "'m receiver_state => 'm list"
   16.11 -  rsent         :: "'m receiver_state => bool multiset"
   16.12 -  rrcvd         :: "'m receiver_state => 'm packet multiset"
   16.13 -  rbit          :: "'m receiver_state => bool"
   16.14 -  rsending      :: "'m receiver_state => bool"
   16.15 +  receiver_asig :: 'm action signature
   16.16 +  receiver_trans:: ('m action, 'm receiver_state)transition set
   16.17 +  receiver_ioa  :: ('m action, 'm receiver_state)ioa
   16.18 +  rq            :: 'm receiver_state => 'm list
   16.19 +  rsent         :: 'm receiver_state => bool multiset
   16.20 +  rrcvd         :: 'm receiver_state => 'm packet multiset
   16.21 +  rbit          :: 'm receiver_state => bool
   16.22 +  rsending      :: 'm receiver_state => bool
   16.23  
   16.24  defs
   16.25  
    17.1 --- a/src/HOL/IOA/NTP/Sender.thy	Thu Nov 30 12:58:44 1995 +0100
    17.2 +++ b/src/HOL/IOA/NTP/Sender.thy	Fri Dec 01 12:03:13 1995 +0100
    17.3 @@ -15,13 +15,13 @@
    17.4  
    17.5  consts
    17.6  
    17.7 -sender_asig   :: "'m action signature"
    17.8 -sender_trans  :: "('m action, 'm sender_state)transition set"
    17.9 -sender_ioa    :: "('m action, 'm sender_state)ioa"
   17.10 -sq            :: "'m sender_state => 'm list"
   17.11 -ssent,srcvd   :: "'m sender_state => bool multiset"
   17.12 -sbit          :: "'m sender_state => bool"
   17.13 -ssending      :: "'m sender_state => bool"
   17.14 +sender_asig   :: 'm action signature
   17.15 +sender_trans  :: ('m action, 'm sender_state)transition set
   17.16 +sender_ioa    :: ('m action, 'm sender_state)ioa
   17.17 +sq            :: 'm sender_state => 'm list
   17.18 +ssent,srcvd   :: 'm sender_state => bool multiset
   17.19 +sbit          :: 'm sender_state => bool
   17.20 +ssending      :: 'm sender_state => bool
   17.21  
   17.22  defs
   17.23  
    18.1 --- a/src/HOL/IOA/NTP/Spec.thy	Thu Nov 30 12:58:44 1995 +0100
    18.2 +++ b/src/HOL/IOA/NTP/Spec.thy	Fri Dec 01 12:03:13 1995 +0100
    18.3 @@ -10,9 +10,9 @@
    18.4  
    18.5  consts
    18.6  
    18.7 -spec_sig   :: "'m action signature"
    18.8 -spec_trans :: "('m action, 'm list)transition set"
    18.9 -spec_ioa   :: "('m action, 'm list)ioa"
   18.10 +spec_sig   :: 'm action signature
   18.11 +spec_trans :: ('m action, 'm list)transition set
   18.12 +spec_ioa   :: ('m action, 'm list)ioa
   18.13  
   18.14  defs
   18.15  
    19.1 --- a/src/HOL/Lambda/Eta.thy	Thu Nov 30 12:58:44 1995 +0100
    19.2 +++ b/src/HOL/Lambda/Eta.thy	Fri Dec 01 12:03:13 1995 +0100
    19.3 @@ -7,11 +7,11 @@
    19.4  *)
    19.5  
    19.6  Eta = ParRed + Commutation +
    19.7 -consts free :: "db => nat => bool"
    19.8 -       decr :: "[db,nat] => db"
    19.9 +consts free :: db => nat => bool
   19.10 +       decr :: [db,nat] => db
   19.11         eta  :: "(db * db) set"
   19.12  
   19.13 -syntax  "-e>", "-e>>", "-e>=" , "->=" :: "[db,db] => bool" (infixl 50)
   19.14 +syntax  "-e>", "-e>>", "-e>=" , "->=" :: [db,db] => bool (infixl 50)
   19.15  
   19.16  translations
   19.17    "s -e>  t" == "(s,t) : eta"
    20.1 --- a/src/HOL/Lambda/Lambda.thy	Thu Nov 30 12:58:44 1995 +0100
    20.2 +++ b/src/HOL/Lambda/Lambda.thy	Fri Dec 01 12:03:13 1995 +0100
    20.3 @@ -12,11 +12,11 @@
    20.4  datatype db = Var nat | "@" db db (infixl 200) | Fun db
    20.5  
    20.6  consts
    20.7 -  subst  :: "[db,db,nat]=>db" ("_[_'/_]" [300,0,0] 300)
    20.8 -  lift   :: "[db,nat] => db"
    20.9 +  subst  :: [db,db,nat]=>db ("_[_'/_]" [300,0,0] 300)
   20.10 +  lift   :: [db,nat] => db
   20.11    (* optimized versions *)
   20.12 -  substn :: "[db,db,nat] => db"
   20.13 -  liftn  :: "[nat,db,nat] => db"
   20.14 +  substn :: [db,db,nat] => db
   20.15 +  liftn  :: [nat,db,nat] => db
   20.16  
   20.17  primrec lift db
   20.18    lift_Var "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
   20.19 @@ -42,7 +42,7 @@
   20.20  
   20.21  consts  beta :: "(db * db) set"
   20.22  
   20.23 -syntax  "->", "->>" :: "[db,db] => bool" (infixl 50)
   20.24 +syntax  "->", "->>" :: [db,db] => bool (infixl 50)
   20.25  
   20.26  translations
   20.27    "s -> t"  == "(s,t) : beta"
    21.1 --- a/src/HOL/Lambda/ParRed.thy	Thu Nov 30 12:58:44 1995 +0100
    21.2 +++ b/src/HOL/Lambda/ParRed.thy	Fri Dec 01 12:03:13 1995 +0100
    21.3 @@ -10,7 +10,7 @@
    21.4  
    21.5  consts  par_beta :: "(db * db) set"
    21.6  
    21.7 -syntax  "=>" :: "[db,db] => bool" (infixl 50)
    21.8 +syntax  "=>" :: [db,db] => bool (infixl 50)
    21.9  
   21.10  translations
   21.11    "s => t" == "(s,t) : par_beta"
   21.12 @@ -23,8 +23,8 @@
   21.13      beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => s'[t'/0]"
   21.14  
   21.15  consts
   21.16 -  cd  :: "db => db"
   21.17 -  deFun :: "db => db"
   21.18 +  cd  :: db => db
   21.19 +  deFun :: db => db
   21.20  
   21.21  primrec cd db
   21.22    cd_Var "cd(Var n) = Var n"
    22.1 --- a/src/HOL/MiniML/I.thy	Thu Nov 30 12:58:44 1995 +0100
    22.2 +++ b/src/HOL/MiniML/I.thy	Fri Dec 01 12:03:13 1995 +0100
    22.3 @@ -8,7 +8,7 @@
    22.4  I = W +
    22.5  
    22.6  consts
    22.7 -	I :: "[expr, type_expr list, nat, subst] => result_W"
    22.8 +	I :: [expr, type_expr list, nat, subst] => result_W
    22.9  
   22.10  primrec I expr
   22.11          I_Var	"I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
    23.1 --- a/src/HOL/MiniML/Maybe.thy	Thu Nov 30 12:58:44 1995 +0100
    23.2 +++ b/src/HOL/MiniML/Maybe.thy	Fri Dec 01 12:03:13 1995 +0100
    23.3 @@ -10,7 +10,7 @@
    23.4  
    23.5  datatype 'a maybe =  Ok 'a | Fail
    23.6  
    23.7 -consts bind :: "['a maybe, 'a => 'b maybe] => 'b maybe" (infixl 60)
    23.8 +consts bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
    23.9  
   23.10  defs
   23.11    bind_def "m bind f == case m of Ok r => f r | Fail => Fail"
    24.1 --- a/src/HOL/MiniML/MiniML.thy	Thu Nov 30 12:58:44 1995 +0100
    24.2 +++ b/src/HOL/MiniML/MiniML.thy	Fri Dec 01 12:03:13 1995 +0100
    24.3 @@ -16,7 +16,7 @@
    24.4  consts
    24.5  	has_type :: "(type_expr list * expr * type_expr)set"
    24.6  syntax
    24.7 -        "@has_type" :: "[type_expr list, expr, type_expr] => bool"
    24.8 +        "@has_type" :: [type_expr list, expr, type_expr] => bool
    24.9                         ("((_) |-/ (_) :: (_))" 60)
   24.10  translations 
   24.11          "a |- e :: t" == "(a,e,t):has_type"
    25.1 --- a/src/HOL/MiniML/Type.thy	Thu Nov 30 12:58:44 1995 +0100
    25.2 +++ b/src/HOL/MiniML/Type.thy	Fri Dec 01 12:03:13 1995 +0100
    25.3 @@ -29,13 +29,13 @@
    25.4  
    25.5  (* identity *)
    25.6  consts
    25.7 -	id_subst :: "subst"
    25.8 +	id_subst :: subst
    25.9  defs
   25.10  	id_subst_def "id_subst == (%n.TVar n)"
   25.11  
   25.12  (* extension of substitution to type structures *)
   25.13  consts
   25.14 -	app_subst :: "[subst, 'a::type_struct] => 'a::type_struct" ("$")
   25.15 +	app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
   25.16  
   25.17  rules
   25.18  	app_subst_TVar  "$ s (TVar n) = s n" 
   25.19 @@ -45,7 +45,7 @@
   25.20    
   25.21  (* free_tv s: the type variables occuring freely in the type structure s *)
   25.22  consts
   25.23 -	free_tv :: "['a::type_struct] => nat set"
   25.24 +	free_tv :: ['a::type_struct] => nat set
   25.25  
   25.26  rules
   25.27  	free_tv_TVar	"free_tv (TVar m) = {m}"
   25.28 @@ -55,13 +55,13 @@
   25.29  
   25.30  (* domain of a substitution *)
   25.31  consts
   25.32 -	dom :: "subst => nat set"
   25.33 +	dom :: subst => nat set
   25.34  defs
   25.35  	dom_def 	"dom s == {n. s n ~= TVar n}" 
   25.36  
   25.37  (* codomain of a substitutions: the introduced variables *)
   25.38  consts
   25.39 -     cod :: "subst => nat set"
   25.40 +     cod :: subst => nat set
   25.41  defs
   25.42  	cod_def		"cod s == (UN m:dom s. free_tv (s m))"
   25.43  
   25.44 @@ -72,13 +72,13 @@
   25.45     structure s, i.e. whether n is greater than any type variable 
   25.46     occuring in the type structure *)
   25.47  consts
   25.48 -	new_tv :: "[nat,'a::type_struct] => bool"
   25.49 +	new_tv :: [nat,'a::type_struct] => bool
   25.50  defs
   25.51          new_tv_def      "new_tv n ts == ! m. m:free_tv ts --> m<n"
   25.52  
   25.53  (* unification algorithm mgu *)
   25.54  consts
   25.55 -	mgu :: "[type_expr,type_expr] => subst maybe"
   25.56 +	mgu :: [type_expr,type_expr] => subst maybe
   25.57  rules
   25.58  	mgu_eq 	 "mgu t1 t2 = Ok u ==> $ u t1 = $ u t2"
   25.59  	mgu_mg 	 "[| (mgu t1 t2) = Ok u; $ s t1 = $ s t2 |] ==>
    26.1 --- a/src/HOL/MiniML/W.thy	Thu Nov 30 12:58:44 1995 +0100
    26.2 +++ b/src/HOL/MiniML/W.thy	Fri Dec 01 12:03:13 1995 +0100
    26.3 @@ -13,7 +13,7 @@
    26.4  
    26.5  (* type inference algorithm W *)
    26.6  consts
    26.7 -	W :: "[expr, type_expr list, nat] => result_W"
    26.8 +	W :: [expr, type_expr list, nat] => result_W
    26.9  
   26.10  primrec W expr
   26.11    W_Var	"W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
    27.1 --- a/src/HOL/ex/BT.thy	Thu Nov 30 12:58:44 1995 +0100
    27.2 +++ b/src/HOL/ex/BT.thy	Fri Dec 01 12:03:13 1995 +0100
    27.3 @@ -11,13 +11,13 @@
    27.4  datatype 'a bt = Lf  |  Br 'a ('a bt) ('a bt)
    27.5    
    27.6  consts
    27.7 -    n_nodes	:: "'a bt => nat"
    27.8 -    n_leaves   	:: "'a bt => nat"
    27.9 -    reflect 	:: "'a bt => 'a bt"
   27.10 -    bt_map      :: "('a=>'b) => ('a bt => 'b bt)"
   27.11 -    preorder    :: "'a bt => 'a list"
   27.12 -    inorder     :: "'a bt => 'a list"
   27.13 -    postorder   :: "'a bt => 'a list"
   27.14 +    n_nodes	:: 'a bt => nat
   27.15 +    n_leaves   	:: 'a bt => nat
   27.16 +    reflect 	:: 'a bt => 'a bt
   27.17 +    bt_map      :: ('a=>'b) => ('a bt => 'b bt)
   27.18 +    preorder    :: 'a bt => 'a list
   27.19 +    inorder     :: 'a bt => 'a list
   27.20 +    postorder   :: 'a bt => 'a list
   27.21  
   27.22  primrec n_nodes bt
   27.23    n_nodes_Lf "n_nodes (Lf) = 0"
    28.1 --- a/src/HOL/ex/InSort.thy	Thu Nov 30 12:58:44 1995 +0100
    28.2 +++ b/src/HOL/ex/InSort.thy	Fri Dec 01 12:03:13 1995 +0100
    28.3 @@ -9,8 +9,8 @@
    28.4  InSort  =  Sorting +
    28.5  
    28.6  consts
    28.7 -  ins :: "[['a,'a]=>bool, 'a, 'a list] => 'a list"
    28.8 -  insort :: "[['a,'a]=>bool, 'a list] => 'a list"
    28.9 +  ins :: [['a,'a]=>bool, 'a, 'a list] => 'a list
   28.10 +  insort :: [['a,'a]=>bool, 'a list] => 'a list
   28.11  
   28.12  primrec ins List.list
   28.13    ins_Nil  "ins f x [] = [x]"
    29.1 --- a/src/HOL/ex/LList.thy	Thu Nov 30 12:58:44 1995 +0100
    29.2 +++ b/src/HOL/ex/LList.thy	Fri Dec 01 12:03:13 1995 +0100
    29.3 @@ -32,34 +32,34 @@
    29.4     llist :: (term)term
    29.5  
    29.6  consts
    29.7 -  list_Fun   :: "['a item set, 'a item set] => 'a item set"
    29.8 +  list_Fun   :: ['a item set, 'a item set] => 'a item set
    29.9    LListD_Fun :: 
   29.10        "[('a item * 'a item)set, ('a item * 'a item)set] => 
   29.11        ('a item * 'a item)set"
   29.12  
   29.13 -  llist      :: "'a item set => 'a item set"
   29.14 +  llist      :: 'a item set => 'a item set
   29.15    LListD     :: "('a item * 'a item)set => ('a item * 'a item)set"
   29.16    llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
   29.17  
   29.18 -  Rep_llist  :: "'a llist => 'a item"
   29.19 -  Abs_llist  :: "'a item => 'a llist"
   29.20 -  LNil       :: "'a llist"
   29.21 -  LCons      :: "['a, 'a llist] => 'a llist"
   29.22 +  Rep_llist  :: 'a llist => 'a item
   29.23 +  Abs_llist  :: 'a item => 'a llist
   29.24 +  LNil       :: 'a llist
   29.25 +  LCons      :: ['a, 'a llist] => 'a llist
   29.26    
   29.27 -  llist_case :: "['b, ['a, 'a llist]=>'b, 'a llist] => 'b"
   29.28 +  llist_case :: ['b, ['a, 'a llist]=>'b, 'a llist] => 'b
   29.29  
   29.30    LList_corec_fun :: "[nat, 'a=>unit+('b item * 'a), 'a] => 'b item"
   29.31    LList_corec     :: "['a, 'a => unit + ('b item * 'a)] => 'b item"
   29.32    llist_corec     :: "['a, 'a => unit + ('b * 'a)] => 'b llist"
   29.33  
   29.34 -  Lmap	     :: "('a item => 'b item) => ('a item => 'b item)"
   29.35 -  lmap	     :: "('a=>'b) => ('a llist => 'b llist)"
   29.36 +  Lmap	     :: ('a item => 'b item) => ('a item => 'b item)
   29.37 +  lmap	     :: ('a=>'b) => ('a llist => 'b llist)
   29.38  
   29.39 -  iterates   :: "['a => 'a, 'a] => 'a llist"
   29.40 +  iterates   :: ['a => 'a, 'a] => 'a llist
   29.41  
   29.42 -  Lconst     :: "'a item => 'a item"
   29.43 -  Lappend    :: "['a item, 'a item] => 'a item"
   29.44 -  lappend    :: "['a llist, 'a llist] => 'a llist"
   29.45 +  Lconst     :: 'a item => 'a item
   29.46 +  Lappend    :: ['a item, 'a item] => 'a item
   29.47 +  lappend    :: ['a llist, 'a llist] => 'a llist
   29.48  
   29.49  
   29.50  coinductive "llist(A)"
    30.1 --- a/src/HOL/ex/MT.thy	Thu Nov 30 12:58:44 1995 +0100
    30.2 +++ b/src/HOL/ex/MT.thy	Fri Dec 01 12:03:13 1995 +0100
    30.3 @@ -46,48 +46,48 @@
    30.4    TyEnv :: term
    30.5  
    30.6  consts
    30.7 -  c_app :: "[Const, Const] => Const"
    30.8 +  c_app :: [Const, Const] => Const
    30.9  
   30.10 -  e_const :: "Const => Ex"
   30.11 -  e_var :: "ExVar => Ex"
   30.12 -  e_fn :: "[ExVar, Ex] => Ex" ("fn _ => _" [0,51] 1000)
   30.13 -  e_fix :: "[ExVar, ExVar, Ex] => Ex" ("fix _ ( _ ) = _" [0,51,51] 1000)
   30.14 -  e_app :: "[Ex, Ex] => Ex" ("_ @ _" [51,51] 1000)
   30.15 -  e_const_fst :: "Ex => Const"
   30.16 +  e_const :: Const => Ex
   30.17 +  e_var :: ExVar => Ex
   30.18 +  e_fn :: [ExVar, Ex] => Ex ("fn _ => _" [0,51] 1000)
   30.19 +  e_fix :: [ExVar, ExVar, Ex] => Ex ("fix _ ( _ ) = _" [0,51,51] 1000)
   30.20 +  e_app :: [Ex, Ex] => Ex ("_ @ _" [51,51] 1000)
   30.21 +  e_const_fst :: Ex => Const
   30.22  
   30.23 -  t_const :: "TyConst => Ty"
   30.24 -  t_fun :: "[Ty, Ty] => Ty" ("_ -> _" [51,51] 1000)
   30.25 +  t_const :: TyConst => Ty
   30.26 +  t_fun :: [Ty, Ty] => Ty ("_ -> _" [51,51] 1000)
   30.27  
   30.28 -  v_const :: "Const => Val"
   30.29 -  v_clos :: "Clos => Val"
   30.30 +  v_const :: Const => Val
   30.31 +  v_clos :: Clos => Val
   30.32    
   30.33 -  ve_emp :: "ValEnv"
   30.34 -  ve_owr :: "[ValEnv, ExVar, Val] => ValEnv" ("_ + { _ |-> _ }" [36,0,0] 50)
   30.35 -  ve_dom :: "ValEnv => ExVar set"
   30.36 -  ve_app :: "[ValEnv, ExVar] => Val"
   30.37 +  ve_emp :: ValEnv
   30.38 +  ve_owr :: [ValEnv, ExVar, Val] => ValEnv ("_ + { _ |-> _ }" [36,0,0] 50)
   30.39 +  ve_dom :: ValEnv => ExVar set
   30.40 +  ve_app :: [ValEnv, ExVar] => Val
   30.41  
   30.42 -  clos_mk :: "[ExVar, Ex, ValEnv] => Clos" ("<| _ , _ , _ |>" [0,0,0] 1000)
   30.43 +  clos_mk :: [ExVar, Ex, ValEnv] => Clos ("<| _ , _ , _ |>" [0,0,0] 1000)
   30.44  
   30.45 -  te_emp :: "TyEnv"
   30.46 -  te_owr :: "[TyEnv, ExVar, Ty] => TyEnv" ("_ + { _ |=> _ }" [36,0,0] 50)
   30.47 -  te_app :: "[TyEnv, ExVar] => Ty"
   30.48 -  te_dom :: "TyEnv => ExVar set"
   30.49 +  te_emp :: TyEnv
   30.50 +  te_owr :: [TyEnv, ExVar, Ty] => TyEnv ("_ + { _ |=> _ }" [36,0,0] 50)
   30.51 +  te_app :: [TyEnv, ExVar] => Ty
   30.52 +  te_dom :: TyEnv => ExVar set
   30.53  
   30.54    eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set"
   30.55    eval_rel :: "((ValEnv * Ex) * Val) set"
   30.56 -  eval :: "[ValEnv, Ex, Val] => bool" ("_ |- _ ---> _" [36,0,36] 50)
   30.57 +  eval :: [ValEnv, Ex, Val] => bool ("_ |- _ ---> _" [36,0,36] 50)
   30.58  
   30.59    elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set"
   30.60    elab_rel :: "((TyEnv * Ex) * Ty) set"
   30.61 -  elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50)
   30.62 +  elab :: [TyEnv, Ex, Ty] => bool ("_ |- _ ===> _" [36,0,36] 50)
   30.63    
   30.64 -  isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50)
   30.65 -  isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _")
   30.66 +  isof :: [Const, Ty] => bool ("_ isof _" [36,36] 50)
   30.67 +  isof_env :: [ValEnv,TyEnv] => bool ("_ isofenv _")
   30.68  
   30.69    hasty_fun :: "(Val * Ty) set => (Val * Ty) set"
   30.70    hasty_rel :: "(Val * Ty) set"
   30.71 -  hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50)
   30.72 -  hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35)
   30.73 +  hasty :: [Val, Ty] => bool ("_ hasty _" [36,36] 50)
   30.74 +  hasty_env :: [ValEnv,TyEnv] => bool ("_ hastyenv _ " [36,36] 35)
   30.75  
   30.76  rules
   30.77  
    31.1 --- a/src/HOL/ex/NatSum.thy	Thu Nov 30 12:58:44 1995 +0100
    31.2 +++ b/src/HOL/ex/NatSum.thy	Fri Dec 01 12:03:13 1995 +0100
    31.3 @@ -7,7 +7,7 @@
    31.4  *)
    31.5  
    31.6  NatSum = Arith +
    31.7 -consts sum     :: "[nat=>nat, nat] => nat"
    31.8 +consts sum     :: [nat=>nat, nat] => nat
    31.9  rules  sum_0      "sum f 0 = 0"
   31.10         sum_Suc    "sum f (Suc n) = f(n) + sum f n"
   31.11  end
    32.1 --- a/src/HOL/ex/Perm.thy	Thu Nov 30 12:58:44 1995 +0100
    32.2 +++ b/src/HOL/ex/Perm.thy	Fri Dec 01 12:03:13 1995 +0100
    32.3 @@ -9,7 +9,7 @@
    32.4  Perm = List +
    32.5  
    32.6  consts  perm    :: "('a list * 'a list) set"   
    32.7 -syntax "@perm"  :: "['a list, 'a list] => bool" ("_ <~~> _"  [50,50] 50)
    32.8 +syntax "@perm"  :: ['a list, 'a list] => bool ("_ <~~> _"  [50,50] 50)
    32.9  
   32.10  translations
   32.11      "x <~~> y" == "(x,y) : perm"
    33.1 --- a/src/HOL/ex/PropLog.thy	Thu Nov 30 12:58:44 1995 +0100
    33.2 +++ b/src/HOL/ex/PropLog.thy	Fri Dec 01 12:03:13 1995 +0100
    33.3 @@ -10,12 +10,12 @@
    33.4  datatype
    33.5      'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
    33.6  consts
    33.7 -  thms :: "'a pl set => 'a pl set"
    33.8 -  "|-" 	:: "['a pl set, 'a pl] => bool"	(infixl 50)
    33.9 -  "|="	:: "['a pl set, 'a pl] => bool"	(infixl 50)
   33.10 -  eval2	:: "['a pl, 'a set] => bool"
   33.11 -  eval	:: "['a set, 'a pl] => bool"	("_[_]" [100,0] 100)
   33.12 -  hyps	:: "['a pl, 'a set] => 'a pl set"
   33.13 +  thms :: 'a pl set => 'a pl set
   33.14 +  "|-" 	:: ['a pl set, 'a pl] => bool	(infixl 50)
   33.15 +  "|="	:: ['a pl set, 'a pl] => bool	(infixl 50)
   33.16 +  eval2	:: ['a pl, 'a set] => bool
   33.17 +  eval	:: ['a set, 'a pl] => bool	("_[_]" [100,0] 100)
   33.18 +  hyps	:: ['a pl, 'a set] => 'a pl set
   33.19  
   33.20  translations
   33.21    "H |- p" == "p : thms(H)"
    34.1 --- a/src/HOL/ex/Puzzle.thy	Thu Nov 30 12:58:44 1995 +0100
    34.2 +++ b/src/HOL/ex/Puzzle.thy	Fri Dec 01 12:03:13 1995 +0100
    34.3 @@ -7,6 +7,6 @@
    34.4  *)
    34.5  
    34.6  Puzzle = Nat +
    34.7 -consts f :: "nat => nat"
    34.8 +consts f :: nat => nat
    34.9  rules  f_ax "f(f(n)) < f(Suc(n))"
   34.10  end
    35.1 --- a/src/HOL/ex/Qsort.thy	Thu Nov 30 12:58:44 1995 +0100
    35.2 +++ b/src/HOL/ex/Qsort.thy	Fri Dec 01 12:03:13 1995 +0100
    35.3 @@ -8,7 +8,7 @@
    35.4  
    35.5  Qsort = Sorting +
    35.6  consts
    35.7 -  qsort  :: "[['a,'a] => bool, 'a list] => 'a list"
    35.8 +  qsort  :: [['a,'a] => bool, 'a list] => 'a list
    35.9  
   35.10  rules
   35.11  
    36.1 --- a/src/HOL/ex/Rec.thy	Thu Nov 30 12:58:44 1995 +0100
    36.2 +++ b/src/HOL/ex/Rec.thy	Fri Dec 01 12:03:13 1995 +0100
    36.3 @@ -1,8 +1,8 @@
    36.4  Rec = Fixedpt +
    36.5  consts
    36.6 -fix	:: "('a=>'a) => 'a"
    36.7 -Dom	:: "(('a=>'b) => ('a=>'b)) => 'a set"
    36.8 -Domf	:: "(('a=>'b) => ('a=>'b)) => 'a set => 'a set"
    36.9 +fix	:: ('a=>'a) => 'a
   36.10 +Dom	:: (('a=>'b) => ('a=>'b)) => 'a set
   36.11 +Domf	:: (('a=>'b) => ('a=>'b)) => 'a set => 'a set
   36.12  rules
   36.13  Domf_def "Domf(F,D) == {y . !f g. (!x:D. f(x)=g(x)) --> F(f,y)=F(g,y)}"
   36.14  Dom_def  "Dom(F) == lfp(Domf(F))"
    37.1 --- a/src/HOL/ex/SList.thy	Thu Nov 30 12:58:44 1995 +0100
    37.2 +++ b/src/HOL/ex/SList.thy	Fri Dec 01 12:03:13 1995 +0100
    37.3 @@ -21,36 +21,36 @@
    37.4  
    37.5  consts
    37.6  
    37.7 -  list      :: "'a item set => 'a item set"
    37.8 -  Rep_list  :: "'a list => 'a item"
    37.9 -  Abs_list  :: "'a item => 'a list"
   37.10 -  NIL       :: "'a item"
   37.11 -  CONS      :: "['a item, 'a item] => 'a item"
   37.12 -  Nil       :: "'a list"
   37.13 -  "#"       :: "['a, 'a list] => 'a list"                   	(infixr 65)
   37.14 -  List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b"
   37.15 -  List_rec  :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b"
   37.16 -  list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
   37.17 -  list_rec  :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
   37.18 -  Rep_map   :: "('b => 'a item) => ('b list => 'a item)"
   37.19 -  Abs_map   :: "('a item => 'b) => 'a item => 'b list"
   37.20 -  null      :: "'a list => bool"
   37.21 -  hd        :: "'a list => 'a"
   37.22 -  tl,ttl    :: "'a list => 'a list"
   37.23 -  mem		:: "['a, 'a list] => bool"			(infixl 55)
   37.24 -  list_all  :: "('a => bool) => ('a list => bool)"
   37.25 -  map       :: "('a=>'b) => ('a list => 'b list)"
   37.26 -  "@"	    :: "['a list, 'a list] => 'a list"			(infixr 65)
   37.27 -  filter    :: "['a => bool, 'a list] => 'a list"
   37.28 +  list      :: 'a item set => 'a item set
   37.29 +  Rep_list  :: 'a list => 'a item
   37.30 +  Abs_list  :: 'a item => 'a list
   37.31 +  NIL       :: 'a item
   37.32 +  CONS      :: ['a item, 'a item] => 'a item
   37.33 +  Nil       :: 'a list
   37.34 +  "#"       :: ['a, 'a list] => 'a list                   	(infixr 65)
   37.35 +  List_case :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
   37.36 +  List_rec  :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
   37.37 +  list_case :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
   37.38 +  list_rec  :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
   37.39 +  Rep_map   :: ('b => 'a item) => ('b list => 'a item)
   37.40 +  Abs_map   :: ('a item => 'b) => 'a item => 'b list
   37.41 +  null      :: 'a list => bool
   37.42 +  hd        :: 'a list => 'a
   37.43 +  tl,ttl    :: 'a list => 'a list
   37.44 +  mem		:: ['a, 'a list] => bool			(infixl 55)
   37.45 +  list_all  :: ('a => bool) => ('a list => bool)
   37.46 +  map       :: ('a=>'b) => ('a list => 'b list)
   37.47 +  "@"	    :: ['a list, 'a list] => 'a list			(infixr 65)
   37.48 +  filter    :: ['a => bool, 'a list] => 'a list
   37.49  
   37.50    (* list Enumeration *)
   37.51  
   37.52 -  "[]"      :: "'a list"                            ("[]")
   37.53 -  "@list"   :: "args => 'a list"                    ("[(_)]")
   37.54 +  "[]"      :: 'a list                            ("[]")
   37.55 +  "@list"   :: args => 'a list                    ("[(_)]")
   37.56  
   37.57    (* Special syntax for list_all and filter *)
   37.58 -  "@Alls"	:: "[idt, 'a list, bool] => bool"	("(2Alls _:_./ _)" 10)
   37.59 -  "@filter"	:: "[idt, 'a list, bool] => 'a list"	("(1[_:_ ./ _])")
   37.60 +  "@Alls"	:: [idt, 'a list, bool] => bool	("(2Alls _:_./ _)" 10)
   37.61 +  "@filter"	:: [idt, 'a list, bool] => 'a list	("(1[_:_ ./ _])")
   37.62  
   37.63  translations
   37.64    "[x, xs]"     == "x#[xs]"
    38.1 --- a/src/HOL/ex/Simult.thy	Thu Nov 30 12:58:44 1995 +0100
    38.2 +++ b/src/HOL/ex/Simult.thy	Fri Dec 01 12:03:13 1995 +0100
    38.3 @@ -21,16 +21,16 @@
    38.4  arities  tree,forest :: (term)term
    38.5  
    38.6  consts
    38.7 -  TF          :: "'a item set => 'a item set"
    38.8 -  FNIL        :: "'a item"
    38.9 -  TCONS,FCONS :: "['a item, 'a item] => 'a item"
   38.10 -  Rep_Tree    :: "'a tree => 'a item"
   38.11 -  Abs_Tree    :: "'a item => 'a tree"
   38.12 -  Rep_Forest  :: "'a forest => 'a item"
   38.13 -  Abs_Forest  :: "'a item => 'a forest"
   38.14 -  Tcons       :: "['a, 'a forest] => 'a tree"
   38.15 -  Fcons       :: "['a tree, 'a forest] => 'a forest"
   38.16 -  Fnil        :: "'a forest"
   38.17 +  TF          :: 'a item set => 'a item set
   38.18 +  FNIL        :: 'a item
   38.19 +  TCONS,FCONS :: ['a item, 'a item] => 'a item
   38.20 +  Rep_Tree    :: 'a tree => 'a item
   38.21 +  Abs_Tree    :: 'a item => 'a tree
   38.22 +  Rep_Forest  :: 'a forest => 'a item
   38.23 +  Abs_Forest  :: 'a item => 'a forest
   38.24 +  Tcons       :: ['a, 'a forest] => 'a tree
   38.25 +  Fcons       :: ['a tree, 'a forest] => 'a forest
   38.26 +  Fnil        :: 'a forest
   38.27    TF_rec      :: "['a item, ['a item , 'a item, 'b]=>'b,     
   38.28                   'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b"
   38.29    tree_rec    :: "['a tree, ['a, 'a forest, 'b]=>'b,          
    39.1 --- a/src/HOL/ex/Sorting.thy	Thu Nov 30 12:58:44 1995 +0100
    39.2 +++ b/src/HOL/ex/Sorting.thy	Fri Dec 01 12:03:13 1995 +0100
    39.3 @@ -8,11 +8,11 @@
    39.4  
    39.5  Sorting = List +
    39.6  consts
    39.7 -  sorted1:: "[['a,'a] => bool, 'a list] => bool"
    39.8 -  sorted :: "[['a,'a] => bool, 'a list] => bool"
    39.9 -  mset   :: "'a list => ('a => nat)"
   39.10 -  total  :: "(['a,'a] => bool) => bool"
   39.11 -  transf :: "(['a,'a] => bool) => bool"
   39.12 +  sorted1:: [['a,'a] => bool, 'a list] => bool
   39.13 +  sorted :: [['a,'a] => bool, 'a list] => bool
   39.14 +  mset   :: 'a list => ('a => nat)
   39.15 +  total  :: (['a,'a] => bool) => bool
   39.16 +  transf :: (['a,'a] => bool) => bool
   39.17  
   39.18  rules
   39.19  
    40.1 --- a/src/HOL/ex/String.thy	Thu Nov 30 12:58:44 1995 +0100
    40.2 +++ b/src/HOL/ex/String.thy	Fri Dec 01 12:03:13 1995 +0100
    40.3 @@ -17,8 +17,8 @@
    40.4    string = "char list"
    40.5  
    40.6  syntax
    40.7 -  "_Char"       :: "xstr => char"       ("CHR _")
    40.8 -  "_String"     :: "xstr => string"     ("_")
    40.9 +  "_Char"       :: xstr => char       ("CHR _")
   40.10 +  "_String"     :: xstr => string     ("_")
   40.11  
   40.12  end
   40.13  
    41.1 --- a/src/HOL/ex/Term.thy	Thu Nov 30 12:58:44 1995 +0100
    41.2 +++ b/src/HOL/ex/Term.thy	Fri Dec 01 12:03:13 1995 +0100
    41.3 @@ -16,14 +16,14 @@
    41.4  arities term :: (term)term
    41.5  
    41.6  consts
    41.7 -  term		:: "'a item set => 'a item set"
    41.8 -  Rep_term	:: "'a term => 'a item"
    41.9 -  Abs_term	:: "'a item => 'a term"
   41.10 -  Rep_Tlist	:: "'a term list => 'a item"
   41.11 -  Abs_Tlist	:: "'a item => 'a term list"
   41.12 -  App		:: "['a, ('a term)list] => 'a term"
   41.13 -  Term_rec	:: "['a item, ['a item , 'a item, 'b list]=>'b] => 'b"
   41.14 -  term_rec	:: "['a term, ['a ,'a term list, 'b list]=>'b] => 'b"
   41.15 +  term		:: 'a item set => 'a item set
   41.16 +  Rep_term	:: 'a term => 'a item
   41.17 +  Abs_term	:: 'a item => 'a term
   41.18 +  Rep_Tlist	:: 'a term list => 'a item
   41.19 +  Abs_Tlist	:: 'a item => 'a term list
   41.20 +  App		:: ['a, ('a term)list] => 'a term
   41.21 +  Term_rec	:: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
   41.22 +  term_rec	:: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
   41.23  
   41.24  inductive "term(A)"
   41.25    intrs