equal
deleted
inserted
replaced
48 val add_0_right = zadd_int0_right |
48 val add_0_right = zadd_int0_right |
49 |
49 |
50 val eq_diff_eq = eq_zdiff_eq |
50 val eq_diff_eq = eq_zdiff_eq |
51 val eqI_rules = [zless_eqI, zeq_eqI, zle_eqI] |
51 val eqI_rules = [zless_eqI, zeq_eqI, zle_eqI] |
52 fun dest_eqI th = |
52 fun dest_eqI th = |
53 #1 (HOLogic.dest_bin "op =" HOLogic.boolT |
53 #1 (HOLogic.dest_bin "op =" HOLogic.boolT |
54 (HOLogic.dest_Trueprop (concl_of th))) |
54 (HOLogic.dest_Trueprop (concl_of th))) |
55 |
55 |
56 val diff_def = zdiff_def |
56 val diff_def = zdiff_def |
57 val minus_add_distrib = zminus_zadd_distrib |
57 val minus_add_distrib = zminus_zadd_distrib |
58 val minus_minus = zminus_zminus |
58 val minus_minus = zminus_zminus |