src/HOL/List.ML
changeset 5278 a903b66822e2
parent 5272 95cfd872fe66
child 5281 f4d16517b360
     1.1 --- a/src/HOL/List.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -243,8 +243,7 @@
     1.4  
     1.5  section "map";
     1.6  
     1.7 -Goal
     1.8 -  "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
     1.9 +Goal "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
    1.10  by (induct_tac "xs" 1);
    1.11  by (Auto_tac);
    1.12  bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
    1.13 @@ -274,8 +273,7 @@
    1.14  qed "rev_map";
    1.15  
    1.16  (* a congruence rule for map: *)
    1.17 -Goal
    1.18 - "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
    1.19 +Goal "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
    1.20  by (rtac impI 1);
    1.21  by (hyp_subst_tac 1);
    1.22  by (induct_tac "ys" 1);
    1.23 @@ -520,8 +518,7 @@
    1.24  
    1.25  section "nth";
    1.26  
    1.27 -Goal
    1.28 -  "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
    1.29 +Goal "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
    1.30  by (induct_tac "n" 1);
    1.31   by (Asm_simp_tac 1);
    1.32   by (rtac allI 1);
    1.33 @@ -596,8 +593,7 @@
    1.34  qed "length_butlast";
    1.35  Addsimps [length_butlast];
    1.36  
    1.37 -Goal
    1.38 -  "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
    1.39 +Goal "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
    1.40  by (induct_tac "xs" 1);
    1.41  by (Auto_tac);
    1.42  qed_spec_mp "butlast_append";
    1.43 @@ -672,8 +668,7 @@
    1.44   by (Auto_tac);
    1.45  qed_spec_mp "drop_all";
    1.46  
    1.47 -Goal 
    1.48 -  "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
    1.49 +Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
    1.50  by (induct_tac "n" 1);
    1.51   by (Auto_tac);
    1.52  by (exhaust_tac "xs" 1);