Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
changeset 57948 75724d71013c
parent 57777 563df8185d98
child 58061 3d060f43accb 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sat Aug 16 12:15:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sat Aug 16 13:23:50 2014 +0200
@@ -129,7 +129,7 @@
     | Blast_Method => blast_tac ctxt
     | Auto_Method => SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt))
     | Auto_Choice_Method =>
-      AtomizeElim.atomize_elim_tac ctxt THEN'
+      Atomize_Elim.atomize_elim_tac ctxt THEN'
       SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt addSIs @{thms choice}))
     | Force_Method => SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt))
     | Linarith_Method =>
isabelle