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.ML
changeset 54503 b490e15a5e19
parent 52629 d6f2a7c196f7
child 54504 096f7d452164 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Tue Nov 19 18:14:56 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Tue Nov 19 18:34:04 2013 +0100
@@ -33,9 +33,6 @@
     ArithM |
     BlastM
 
-  (* legacy *)
-  val By_Metis : facts -> byline
-
   val no_label : label
   val no_facts : facts
 
@@ -100,9 +97,6 @@
   ArithM |
   BlastM
 
-(* legacy *)
-fun By_Metis facts = By (facts, MetisM)
-
 val no_label = ("", ~1)
 val no_facts = ([],[])
isabelle