equal
deleted
inserted
replaced
6 structure ab_group_add_cancel_data :> ABEL_CANCEL = |
6 structure ab_group_add_cancel_data :> ABEL_CANCEL = |
7 struct |
7 struct |
8 val ss = simpset_of HOL.thy |
8 val ss = simpset_of HOL.thy |
9 val eq_reflection = thm "eq_reflection" |
9 val eq_reflection = thm "eq_reflection" |
10 |
10 |
11 val sg_ref = Sign.self_ref (sign_of (theory "OrderedGroup")) |
11 val thy_ref = Theory.self_ref (theory "OrderedGroup") |
12 |
12 |
13 val T = TFree("'a", ["OrderedGroup.ab_group_add"]) |
13 val T = TFree("'a", ["OrderedGroup.ab_group_add"]) |
14 |
14 |
15 val restrict_to_left = thm "restrict_to_left" |
15 val restrict_to_left = thm "restrict_to_left" |
16 val add_cancel_21 = thm "add_cancel_21" |
16 val add_cancel_21 = thm "add_cancel_21" |