equal
deleted
inserted
replaced
106 "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)", |
106 "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)", |
107 "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ]; |
107 "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ]; |
108 |
108 |
109 (*Add congruence rules for = (instead of ==) *) |
109 (*Add congruence rules for = (instead of ==) *) |
110 infix 4 addcongs delcongs; |
110 infix 4 addcongs delcongs; |
111 fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]); |
111 fun ss addcongs congs = ss addeqcongs (map standard (congs RL [eq_reflection])); |
112 fun ss delcongs congs = ss deleqcongs (congs RL [eq_reflection]); |
112 fun ss delcongs congs = ss deleqcongs (map standard (congs RL [eq_reflection])); |
113 |
113 |
114 fun Addcongs congs = (simpset := !simpset addcongs congs); |
114 fun Addcongs congs = (simpset := !simpset addcongs congs); |
115 fun Delcongs congs = (simpset := !simpset delcongs congs); |
115 fun Delcongs congs = (simpset := !simpset delcongs congs); |
116 |
116 |
117 fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all; |
117 fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all; |