equal
deleted
inserted
replaced
13 open LList; |
13 open LList; |
14 |
14 |
15 (** Simplification **) |
15 (** Simplification **) |
16 |
16 |
17 val llist_simps = [case_Inl, case_Inr]; |
17 val llist_simps = [case_Inl, case_Inr]; |
18 val llist_ss = univ_ss addsimps llist_simps |
18 val llist_ss = univ_ss delsimps [Pair_eq] |
|
19 addsimps llist_simps |
19 addcongs [split_weak_cong, case_weak_cong] |
20 addcongs [split_weak_cong, case_weak_cong] |
20 setloop (split_tac [expand_split, expand_case]); |
21 setloop (split_tac [expand_split, expand_case]); |
21 |
22 |
22 (** the llist functional **) |
23 (** the llist functional **) |
23 |
24 |