equal
deleted
inserted
replaced
29 struct |
29 struct |
30 val ss = HOL_ss |
30 val ss = HOL_ss |
31 val eq_reflection = eq_reflection |
31 val eq_reflection = eq_reflection |
32 |
32 |
33 val thy = IntDef.thy |
33 val thy = IntDef.thy |
34 val T = Type ("IntDef.int", []) |
34 val T = HOLogic.intT |
35 val zero = Const ("IntDef.int", HOLogic.natT --> T) $ HOLogic.zero |
35 val zero = Const ("IntDef.int", HOLogic.natT --> T) $ HOLogic.zero |
36 val add_cancel_21 = zadd_cancel_21 |
36 val add_cancel_21 = zadd_cancel_21 |
37 val add_cancel_end = zadd_cancel_end |
37 val add_cancel_end = zadd_cancel_end |
38 val add_left_cancel = zadd_left_cancel |
38 val add_left_cancel = zadd_left_cancel |
39 val add_assoc = zadd_assoc |
39 val add_assoc = zadd_assoc |