equal
deleted
inserted
replaced
96 |
96 |
97 (*Add congruence rules for = (instead of ==) *) |
97 (*Add congruence rules for = (instead of ==) *) |
98 infix 4 addcongs; |
98 infix 4 addcongs; |
99 fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]); |
99 fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]); |
100 |
100 |
|
101 fun Addcongs congs = (simpset := !simpset addcongs congs); |
|
102 |
101 (*Add a simpset to a classical set!*) |
103 (*Add a simpset to a classical set!*) |
102 infix 4 addss; |
104 infix 4 addss; |
103 fun cs addss ss = cs addbefore asm_full_simp_tac ss 1; |
105 fun cs addss ss = cs addbefore asm_full_simp_tac ss 1; |
104 |
106 |
105 val mksimps_pairs = |
107 val mksimps_pairs = |