equal
deleted
inserted
replaced
40 by (fast_tac HOL_cs 1); |
40 by (fast_tac HOL_cs 1); |
41 val de_morgan = result(); |
41 val de_morgan = result(); |
42 |
42 |
43 (* Lists *) |
43 (* Lists *) |
44 |
44 |
|
45 val list_ss = simpset_of "List"; |
|
46 |
45 goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))"; |
47 goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))"; |
46 by (List.list.induct_tac "l" 1); |
48 by (List.list.induct_tac "l" 1); |
47 by (simp_tac list_ss 1); |
49 by (simp_tac list_ss 1); |
48 by (simp_tac list_ss 1); |
50 by (simp_tac list_ss 1); |
49 val hd_append =result(); |
51 val hd_append =result(); |