equal
deleted
inserted
replaced
388 let |
388 let |
389 val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm); |
389 val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm); |
390 val thm2 = standard thm1; |
390 val thm2 = standard thm1; |
391 in |
391 in |
392 thy |
392 thy |
393 |> PureThy.store_thm (bthm, thm2) |
393 |> PureThy.store_thm (Binding.name bthm, thm2) |
394 |> snd |
394 |> snd |
395 |> add_hol4_theorem bthy bthm hth |
395 |> add_hol4_theorem bthy bthm hth |
396 end; |
396 end; |
397 in |
397 in |
398 thy |
398 thy |