# HG changeset patch # User wenzelm # Date 1446221670 -3600 # Node ID d05f3d86a758931d5cd379b9ec86b766eebb20da # Parent c0429568593679906b7582224888e165c56a3dc0 tuned signature -- clarified modules; diff -r c04295685936 -r d05f3d86a758 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Fri Oct 30 16:31:37 2015 +0100 +++ b/src/Pure/Isar/attrib.ML Fri Oct 30 17:14:30 2015 +0100 @@ -510,7 +510,7 @@ (* theory setup *) val _ = Theory.setup - (register_config quick_and_dirty_raw #> + (register_config Goal.quick_and_dirty_raw #> register_config Ast.trace_raw #> register_config Ast.stats_raw #> register_config Printer.show_brackets_raw #> diff -r c04295685936 -r d05f3d86a758 src/Pure/goal.ML --- a/src/Pure/goal.ML Fri Oct 30 16:31:37 2015 +0100 +++ b/src/Pure/goal.ML Fri Oct 30 17:14:30 2015 +0100 @@ -6,6 +6,7 @@ signature BASIC_GOAL = sig + val quick_and_dirty: bool Config.T val parallel_proofs: int Unsynchronized.ref val SELECT_GOAL: tactic -> int -> tactic val PREFER_GOAL: tactic -> int -> tactic @@ -38,6 +39,7 @@ ({prems: thm list, context: Proof.context} -> tactic) -> thm val prove_global: theory -> string list -> term list -> term -> ({prems: thm list, context: Proof.context} -> tactic) -> thm + val quick_and_dirty_raw: Config.raw val prove_sorry: Proof.context -> string list -> term list -> term -> ({prems: thm list, context: Proof.context} -> tactic) -> thm val prove_sorry_global: theory -> string list -> term list -> term -> @@ -250,6 +252,12 @@ fun prove_global thy xs asms prop tac = Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac); + +(* skip proofs *) + +val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", @{here}); +val quick_and_dirty = Config.bool quick_and_dirty_raw; + fun prove_sorry ctxt xs asms prop tac = if Config.get ctxt quick_and_dirty then prove ctxt xs asms prop (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt)) diff -r c04295685936 -r d05f3d86a758 src/Pure/skip_proof.ML --- a/src/Pure/skip_proof.ML Fri Oct 30 16:31:37 2015 +0100 +++ b/src/Pure/skip_proof.ML Fri Oct 30 17:14:30 2015 +0100 @@ -4,9 +4,6 @@ Skip proof via oracle invocation. *) -val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", @{here}); -val quick_and_dirty = Config.bool quick_and_dirty_raw; - signature SKIP_PROOF = sig val report: Proof.context -> unit