equal
deleted
inserted
replaced
182 equal_elim (symmetric rew_imp) thm |
182 equal_elim (symmetric rew_imp) thm |
183 |
183 |
184 fun add_final (arg as (thy, thm)) = |
184 fun add_final (arg as (thy, thm)) = |
185 if name = "" |
185 if name = "" |
186 then arg |> Library.swap |
186 then arg |> Library.swap |
187 else (writeln (" " ^ name ^ ": " ^ (string_of_thm thm)); |
187 else (writeln (" " ^ name ^ ": " ^ (Display.string_of_thm thm)); |
188 PureThy.store_thm (name, thm) thy) |
188 PureThy.store_thm (name, thm) thy) |
189 in |
189 in |
190 args |> apsnd (remove_alls frees) |
190 args |> apsnd (remove_alls frees) |
191 |> apsnd undo_imps |
191 |> apsnd undo_imps |
192 |> apsnd standard |
192 |> apsnd standard |