# HG changeset patch # User wenzelm # Date 1329243537 -3600 # Node ID 4cf5a84e2c055e113a3b471950fd3b16f033bbe6 # Parent 3d0629a9ffca633e4644f735f914535b28e8de8a normalized aliases; diff -r 3d0629a9ffca -r 4cf5a84e2c05 src/HOL/Boogie/Tools/boogie_tactics.ML --- a/src/HOL/Boogie/Tools/boogie_tactics.ML Tue Feb 14 17:54:08 2012 +0100 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Tue Feb 14 19:18:57 2012 +0100 @@ -92,7 +92,7 @@ (Rule_Cases.make_common (Proof_Context.theory_of ctxt, Thm.prop_of (Rule_Cases.internalize_params st)) (map (rpair []) names)) - Tactical.all_tac st)) + all_tac st)) in val setup_boogie_cases = Method.setup @{binding boogie_cases} (Scan.succeed boogie_cases) diff -r 3d0629a9ffca -r 4cf5a84e2c05 src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Tue Feb 14 17:54:08 2012 +0100 +++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Feb 14 19:18:57 2012 +0100 @@ -39,8 +39,8 @@ {outcome: SMT_Failure.failure option, used_facts: ('a * thm) list} (*tactic*) - val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic - val smt_tac': Proof.context -> thm list -> int -> Tactical.tactic + val smt_tac: Proof.context -> thm list -> int -> tactic + val smt_tac': Proof.context -> thm list -> int -> tactic (*setup*) val setup: theory -> theory @@ -357,7 +357,7 @@ fun tag_prems thms = map (pair ~1 o pair NONE) thms fun resolve (SOME thm) = Tactic.rtac thm 1 - | resolve NONE = Tactical.no_tac + | resolve NONE = no_tac fun tac prove ctxt rules = CONVERSION (SMT_Normalize.atomize_conv ctxt) diff -r 3d0629a9ffca -r 4cf5a84e2c05 src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Tue Feb 14 17:54:08 2012 +0100 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Tue Feb 14 19:18:57 2012 +0100 @@ -724,14 +724,14 @@ THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))), Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' => Z3_Proof_Tools.by_tac ( - (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac) + (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac) THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset) THEN_ALL_NEW ( NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt') ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))), Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' => Z3_Proof_Tools.by_tac ( - (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac) + (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac) THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset) THEN_ALL_NEW ( NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt') @@ -740,7 +740,7 @@ Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt [] (fn ctxt' => Z3_Proof_Tools.by_tac ( - (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac) + (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac) THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac simpset) THEN_ALL_NEW ( NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')