src/HOL/List.ML
changeset 5043 3fdc881e8ff9
parent 4935 1694e2daef8f
child 5077 71043526295f
     1.1 --- a/src/HOL/List.ML	Wed Jun 17 10:49:24 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Wed Jun 17 10:49:45 1998 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  
     1.5  (** "lists": the list-forming operator over sets **)
     1.6  
     1.7 -Goalw lists.defs "!!A B. A<=B ==> lists A <= lists B";
     1.8 +Goalw lists.defs "A<=B ==> lists A <= lists B";
     1.9  by (rtac lfp_mono 1);
    1.10  by (REPEAT (ares_tac basic_monos 1));
    1.11  qed "lists_mono";
    1.12 @@ -37,7 +37,7 @@
    1.13  AddSEs [listsE];
    1.14  AddSIs lists.intrs;
    1.15  
    1.16 -Goal "!!l. l: lists A ==> l: lists B --> l: lists (A Int B)";
    1.17 +Goal "l: lists A ==> l: lists B --> l: lists (A Int B)";
    1.18  by (etac lists.induct 1);
    1.19  by (ALLGOALS Blast_tac);
    1.20  qed_spec_mp "lists_IntI";
    1.21 @@ -88,7 +88,7 @@
    1.22  qed "length_rev";
    1.23  Addsimps [length_rev];
    1.24  
    1.25 -Goal "!!xs. xs ~= [] ==> length(tl xs) = (length xs) - 1";
    1.26 +Goal "xs ~= [] ==> length(tl xs) = (length xs) - 1";
    1.27  by (exhaust_tac "xs" 1);
    1.28  by (ALLGOALS Asm_full_simp_tac);
    1.29  qed "length_tl";
    1.30 @@ -209,7 +209,7 @@
    1.31  by (ALLGOALS Asm_simp_tac);
    1.32  qed "hd_append";
    1.33  
    1.34 -Goal "!!xs. xs ~= [] ==> hd(xs @ ys) = hd xs";
    1.35 +Goal "xs ~= [] ==> hd(xs @ ys) = hd xs";
    1.36  by (asm_simp_tac (simpset() addsimps [hd_append]
    1.37                             addsplits [split_list_case]) 1);
    1.38  qed "hd_append2";
    1.39 @@ -219,7 +219,7 @@
    1.40  by (simp_tac (simpset() addsplits [split_list_case]) 1);
    1.41  qed "tl_append";
    1.42  
    1.43 -Goal "!!xs. xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys";
    1.44 +Goal "xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys";
    1.45  by (asm_simp_tac (simpset() addsimps [tl_append]
    1.46                             addsplits [split_list_case]) 1);
    1.47  qed "tl_append2";
    1.48 @@ -568,12 +568,12 @@
    1.49  by (ALLGOALS Asm_simp_tac);
    1.50  qed_spec_mp "in_set_butlastD";
    1.51  
    1.52 -Goal "!!xs. x:set(butlast xs) ==> x:set(butlast(xs@ys))";
    1.53 +Goal "x:set(butlast xs) ==> x:set(butlast(xs@ys))";
    1.54  by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
    1.55  by (blast_tac (claset() addDs [in_set_butlastD]) 1);
    1.56  qed "in_set_butlast_appendI1";
    1.57  
    1.58 -Goal "!!xs. x:set(butlast ys) ==> x:set(butlast(xs@ys))";
    1.59 +Goal "x:set(butlast ys) ==> x:set(butlast(xs@ys))";
    1.60  by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
    1.61  by (Clarify_tac 1);
    1.62  by (Full_simp_tac 1);
    1.63 @@ -792,7 +792,7 @@
    1.64  by (ALLGOALS Asm_full_simp_tac);
    1.65  val lemma = result();
    1.66  
    1.67 -Goal "!!n. n ~= 0 ==> set(replicate n x) = {x}";
    1.68 +Goal "n ~= 0 ==> set(replicate n x) = {x}";
    1.69  by (fast_tac (claset() addSDs [not0_implies_Suc] addSIs [lemma]) 1);
    1.70  qed "set_replicate";
    1.71  Addsimps [set_replicate];