# HG changeset patch
# User blanchet
# Date 1342035799 -7200
# Node ID 2bd242c56c90931f5cabd8d5f5555614e5ca3854
# Parent  b6eb45a52c286928ddc855e8cbd7a5bac54ff75b
dummy implementation

diff -r b6eb45a52c28 -r 2bd242c56c90 src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 11 21:43:19 2012 +0200
@@ -6,8 +6,43 @@
 
 signature SLEDGEHAMMER_FILTER_MASH =
 sig
+  val reset : unit -> unit
+  val can_suggest : unit -> bool
+  val can_learn_thy : theory -> bool
+  val learn_thy : theory -> real -> unit
+  val learn_proof : theory -> term -> thm list -> unit
 end;
 
 structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
 struct
+
+fun mash_reset () =
+  tracing "MaSh RESET"
+
+fun mash_add fact (access, feats, deps) =
+  tracing ("MaSh ADD " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^
+           space_implode " " feats ^ "; " ^ space_implode " " deps)
+
+fun mash_del fact =
+  tracing ("MaSh DEL " ^ fact)
+
+fun mash_suggest fact (access, feats) =
+  tracing ("MaSh SUGGEST " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^
+           space_implode " " feats)
+
+fun reset () =
+  ()
+
+fun can_suggest () =
+  true
+
+fun can_learn_thy thy =
+  true
+
+fun learn_thy thy timeout =
+  ()
+
+fun learn_proof theory t thms =
+  ()
+
 end;