src/HOL/ex/SList.thy
changeset 1376 92f83b9d17e1
parent 1266 3ae9fe3c0f68
child 1476 608483c2122a
     1.1 --- a/src/HOL/ex/SList.thy	Thu Nov 30 12:58:44 1995 +0100
     1.2 +++ b/src/HOL/ex/SList.thy	Fri Dec 01 12:03:13 1995 +0100
     1.3 @@ -21,36 +21,36 @@
     1.4  
     1.5  consts
     1.6  
     1.7 -  list      :: "'a item set => 'a item set"
     1.8 -  Rep_list  :: "'a list => 'a item"
     1.9 -  Abs_list  :: "'a item => 'a list"
    1.10 -  NIL       :: "'a item"
    1.11 -  CONS      :: "['a item, 'a item] => 'a item"
    1.12 -  Nil       :: "'a list"
    1.13 -  "#"       :: "['a, 'a list] => 'a list"                   	(infixr 65)
    1.14 -  List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b"
    1.15 -  List_rec  :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b"
    1.16 -  list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
    1.17 -  list_rec  :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
    1.18 -  Rep_map   :: "('b => 'a item) => ('b list => 'a item)"
    1.19 -  Abs_map   :: "('a item => 'b) => 'a item => 'b list"
    1.20 -  null      :: "'a list => bool"
    1.21 -  hd        :: "'a list => 'a"
    1.22 -  tl,ttl    :: "'a list => 'a list"
    1.23 -  mem		:: "['a, 'a list] => bool"			(infixl 55)
    1.24 -  list_all  :: "('a => bool) => ('a list => bool)"
    1.25 -  map       :: "('a=>'b) => ('a list => 'b list)"
    1.26 -  "@"	    :: "['a list, 'a list] => 'a list"			(infixr 65)
    1.27 -  filter    :: "['a => bool, 'a list] => 'a list"
    1.28 +  list      :: 'a item set => 'a item set
    1.29 +  Rep_list  :: 'a list => 'a item
    1.30 +  Abs_list  :: 'a item => 'a list
    1.31 +  NIL       :: 'a item
    1.32 +  CONS      :: ['a item, 'a item] => 'a item
    1.33 +  Nil       :: 'a list
    1.34 +  "#"       :: ['a, 'a list] => 'a list                   	(infixr 65)
    1.35 +  List_case :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
    1.36 +  List_rec  :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
    1.37 +  list_case :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
    1.38 +  list_rec  :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
    1.39 +  Rep_map   :: ('b => 'a item) => ('b list => 'a item)
    1.40 +  Abs_map   :: ('a item => 'b) => 'a item => 'b list
    1.41 +  null      :: 'a list => bool
    1.42 +  hd        :: 'a list => 'a
    1.43 +  tl,ttl    :: 'a list => 'a list
    1.44 +  mem		:: ['a, 'a list] => bool			(infixl 55)
    1.45 +  list_all  :: ('a => bool) => ('a list => bool)
    1.46 +  map       :: ('a=>'b) => ('a list => 'b list)
    1.47 +  "@"	    :: ['a list, 'a list] => 'a list			(infixr 65)
    1.48 +  filter    :: ['a => bool, 'a list] => 'a list
    1.49  
    1.50    (* list Enumeration *)
    1.51  
    1.52 -  "[]"      :: "'a list"                            ("[]")
    1.53 -  "@list"   :: "args => 'a list"                    ("[(_)]")
    1.54 +  "[]"      :: 'a list                            ("[]")
    1.55 +  "@list"   :: args => 'a list                    ("[(_)]")
    1.56  
    1.57    (* Special syntax for list_all and filter *)
    1.58 -  "@Alls"	:: "[idt, 'a list, bool] => bool"	("(2Alls _:_./ _)" 10)
    1.59 -  "@filter"	:: "[idt, 'a list, bool] => 'a list"	("(1[_:_ ./ _])")
    1.60 +  "@Alls"	:: [idt, 'a list, bool] => bool	("(2Alls _:_./ _)" 10)
    1.61 +  "@filter"	:: [idt, 'a list, bool] => 'a list	("(1[_:_ ./ _])")
    1.62  
    1.63  translations
    1.64    "[x, xs]"     == "x#[xs]"