summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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);