--- a/src/HOL/Hilbert_Choice.thy Mon Sep 29 12:30:12 2014 +0200
+++ b/src/HOL/Hilbert_Choice.thy Mon Sep 29 14:32:30 2014 +0200
@@ -111,19 +111,6 @@
qed
-subsection {* A skolemization tactic and proof method *}
-
-ML {*
-fun moura_tac ctxt =
- Atomize_Elim.atomize_elim_tac ctxt THEN'
- SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice bchoice}) THEN ALLGOALS (blast_tac ctxt));
-*}
-
-method_setup moura = {*
- Scan.succeed (SIMPLE_METHOD' o moura_tac)
-*} "solve skolemization goals, especially those arising from Z3 proofs"
-
-
subsection {*Function Inverse*}
lemma inv_def: "inv f = (%y. SOME x. f x = y)"