256 structure HOL4Rewrites = TheoryDataFun(HOL4RewritesArgs); |
256 structure HOL4Rewrites = TheoryDataFun(HOL4RewritesArgs); |
257 |
257 |
258 val hol4_debug = ref false |
258 val hol4_debug = ref false |
259 fun message s = if !hol4_debug then writeln s else () |
259 fun message s = if !hol4_debug then writeln s else () |
260 |
260 |
261 fun add_hol4_rewrite (context, th) = |
261 fun add_hol4_rewrite (Context.Theory thy, th) = |
262 let |
262 let |
263 val thy = Context.the_theory context; |
|
264 val _ = message "Adding HOL4 rewrite" |
263 val _ = message "Adding HOL4 rewrite" |
265 val th1 = th RS eq_reflection |
264 val th1 = th RS eq_reflection |
266 val current_rews = HOL4Rewrites.get thy |
265 val current_rews = HOL4Rewrites.get thy |
267 val new_rews = insert Thm.eq_thm th1 current_rews |
266 val new_rews = insert Thm.eq_thm th1 current_rews |
268 val updated_thy = HOL4Rewrites.put new_rews thy |
267 val updated_thy = HOL4Rewrites.put new_rews thy |
269 in |
268 in |
270 (Context.Theory updated_thy,th1) |
269 (Context.Theory updated_thy,th1) |
271 end; |
270 end |
|
271 | add_hol4_rewrite (context, th) = (context, th RS eq_reflection); |
272 |
272 |
273 fun ignore_hol4 bthy bthm thy = |
273 fun ignore_hol4 bthy bthm thy = |
274 let |
274 let |
275 val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm) |
275 val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm) |
276 val curmaps = HOL4Maps.get thy |
276 val curmaps = HOL4Maps.get thy |