equal
deleted
inserted
replaced
253 Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac); |
253 Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac); |
254 |
254 |
255 |
255 |
256 (* skip proofs *) |
256 (* skip proofs *) |
257 |
257 |
258 val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", @{here}); |
258 val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", \<^here>); |
259 val quick_and_dirty = Config.bool quick_and_dirty_raw; |
259 val quick_and_dirty = Config.bool quick_and_dirty_raw; |
260 |
260 |
261 fun prove_sorry ctxt xs asms prop tac = |
261 fun prove_sorry ctxt xs asms prop tac = |
262 if Config.get ctxt quick_and_dirty then |
262 if Config.get ctxt quick_and_dirty then |
263 prove ctxt xs asms prop (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt)) |
263 prove ctxt xs asms prop (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt)) |