equal
deleted
inserted
replaced
1 (* Title: HOL/OrderedGroup.ML |
1 (* Title: HOL/OrderedGroup.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Steven Obua, Tobias Nipkow, Technische Universitaet Mnchen |
3 Author: Steven Obua, Tobias Nipkow, Technische Universitaet Muenchen |
4 *) |
4 *) |
5 |
5 |
6 structure ab_group_add_cancel_data :> ABEL_CANCEL = |
6 structure ab_group_add_cancel_data :> ABEL_CANCEL = |
7 struct |
7 struct |
8 |
8 |
9 (*** Term order for abelian groups ***) |
9 (*** Term order for abelian groups ***) |
10 |
10 |
11 fun agrp_ord a = find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus"]; |
11 fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus"] |
|
12 | agrp_ord _ = ~1; |
12 |
13 |
13 fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS); |
14 fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS); |
14 |
15 |
15 local |
16 local |
16 val ac1 = mk_meta_eq (thm "add_assoc"); |
17 val ac1 = mk_meta_eq (thm "add_assoc"); |