eliminate get_def; Isabelle99-2
authorwenzelm
Thu Feb 15 17:18:54 2001 +0100 (2001-02-15)
changeset 111453e47692e3a3e
parent 11144 f53ea84bab23
child 11146 449e1a1bb7a8
eliminate get_def;
src/ZF/List.ML
     1.1 --- a/src/ZF/List.ML	Thu Feb 15 16:12:27 2001 +0100
     1.2 +++ b/src/ZF/List.ML	Thu Feb 15 17:18:54 2001 +0100
     1.3 @@ -99,7 +99,7 @@
     1.4  
     1.5  (** map **)
     1.6  
     1.7 -val prems = Goalw [get_def (the_context ()) "map_list"] 
     1.8 +val prems = Goalw [thm "map_list_def"]
     1.9      "[| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
    1.10  by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1));
    1.11  qed "map_type";
    1.12 @@ -111,21 +111,21 @@
    1.13  
    1.14  (** length **)
    1.15  
    1.16 -Goalw [get_def (the_context ()) "length_list"] 
    1.17 +Goalw [thm "length_list_def"]
    1.18      "l: list(A) ==> length(l) : nat";
    1.19  by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1));
    1.20  qed "length_type";
    1.21  
    1.22  (** app **)
    1.23  
    1.24 -Goalw [get_def (the_context ()) "op @_list"] 
    1.25 +Goalw [thm "op @_list_def"]
    1.26      "[| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)";
    1.27  by (REPEAT (ares_tac [list_rec_type, list.Cons_I] 1));
    1.28  qed "app_type";
    1.29  
    1.30  (** rev **)
    1.31  
    1.32 -Goalw [get_def (the_context ()) "rev_list"] 
    1.33 +Goalw [thm "rev_list_def"]
    1.34      "xs: list(A) ==> rev(xs) : list(A)";
    1.35  by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
    1.36  qed "rev_type";
    1.37 @@ -133,7 +133,7 @@
    1.38  
    1.39  (** flat **)
    1.40  
    1.41 -Goalw [get_def (the_context ()) "flat_list"] 
    1.42 +Goalw [thm "flat_list_def"]
    1.43      "ls: list(list(A)) ==> flat(ls) : list(A)";
    1.44  by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
    1.45  qed "flat_type";
    1.46 @@ -141,7 +141,7 @@
    1.47  
    1.48  (** set_of_list **)
    1.49  
    1.50 -Goalw [get_def (the_context ()) "set_of_list_list"] 
    1.51 +Goalw [thm "set_of_list_list_def"]
    1.52      "l: list(A) ==> set_of_list(l) : Pow(A)";
    1.53  by (etac list_rec_type 1);
    1.54  by (ALLGOALS (Blast_tac));
    1.55 @@ -156,7 +156,7 @@
    1.56  
    1.57  (** list_add **)
    1.58  
    1.59 -Goalw [get_def (the_context ()) "list_add_list"] 
    1.60 +Goalw [thm "list_add_list_def"] 
    1.61      "xs: list(nat) ==> list_add(xs) : nat";
    1.62  by (REPEAT (ares_tac [list_rec_type, nat_0I, add_type] 1));
    1.63  qed "list_add_type";