--- a/src/HOL/List.thy Fri Aug 16 11:27:10 1996 +0200
+++ b/src/HOL/List.thy Mon Aug 19 11:12:38 1996 +0200
@@ -6,7 +6,7 @@
Definition of type 'a list as a datatype. This allows primrec to work.
TODO: delete list_all from this theory and from ex/Sorting, etc.
- use setOfList instead
+ use set_of_list instead
*)
List = Arith +
@@ -15,29 +15,29 @@
consts
- "@" :: ['a list, 'a list] => 'a list (infixr 65)
- drop :: [nat, 'a list] => 'a list
- filter :: ['a => bool, 'a list] => 'a list
- flat :: 'a list list => 'a list
- foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b
- hd :: 'a list => 'a
- length :: 'a list => nat
- setOfList :: ('a list => 'a set)
- list_all :: ('a => bool) => ('a list => bool)
- map :: ('a=>'b) => ('a list => 'b list)
- mem :: ['a, 'a list] => bool (infixl 55)
- nth :: [nat, 'a list] => 'a
- take :: [nat, 'a list] => 'a list
- tl,ttl :: 'a list => 'a list
- rev :: 'a list => 'a list
+ "@" :: ['a list, 'a list] => 'a list (infixr 65)
+ drop :: [nat, 'a list] => 'a list
+ filter :: ['a => bool, 'a list] => 'a list
+ flat :: 'a list list => 'a list
+ foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b
+ hd :: 'a list => 'a
+ length :: 'a list => nat
+ set_of_list :: ('a list => 'a set)
+ list_all :: ('a => bool) => ('a list => bool)
+ map :: ('a=>'b) => ('a list => 'b list)
+ mem :: ['a, 'a list] => bool (infixl 55)
+ nth :: [nat, 'a list] => 'a
+ take :: [nat, 'a list] => 'a list
+ tl,ttl :: 'a list => 'a list
+ rev :: 'a list => 'a list
syntax
(* list Enumeration *)
- "@list" :: args => '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]"
@@ -59,9 +59,9 @@
primrec "op mem" list
"x mem [] = False"
"x mem (y#ys) = (if y=x then True else x mem ys)"
-primrec setOfList list
- "setOfList [] = {}"
- "setOfList (x#xs) = insert x (setOfList xs)"
+primrec set_of_list list
+ "set_of_list [] = {}"
+ "set_of_list (x#xs) = insert x (set_of_list xs)"
primrec list_all list
list_all_Nil "list_all P [] = True"
list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"