equal
deleted
inserted
replaced
8 |
8 |
9 open List; |
9 open List; |
10 |
10 |
11 val [Nil_not_Cons,Cons_not_Nil] = list.distinct; |
11 val [Nil_not_Cons,Cons_not_Nil] = list.distinct; |
12 |
12 |
13 bind_thm("Cons_neq_Nil", standard (Cons_not_Nil RS notE)); |
13 bind_thm("Cons_neq_Nil", Cons_not_Nil RS notE); |
14 bind_thm("Nil_neq_Cons", sym RS Cons_neq_Nil); |
14 bind_thm("Nil_neq_Cons", sym RS Cons_neq_Nil); |
15 |
15 |
16 bind_thm("Cons_inject", standard ((hd list.inject) RS iffD1 RS conjE)); |
16 bind_thm("Cons_inject", (hd list.inject) RS iffD1 RS conjE); |
17 |
17 |
18 val list_ss = HOL_ss addsimps list.simps; |
18 val list_ss = HOL_ss addsimps list.simps; |
19 |
19 |
20 goal List.thy "!x. xs ~= x#xs"; |
20 goal List.thy "!x. xs ~= x#xs"; |
21 by (list.induct_tac "xs" 1); |
21 by (list.induct_tac "xs" 1); |