--- a/src/HOL/Metis_Examples/Type_Encodings.thy Thu Dec 01 13:34:12 2011 +0100
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Thu Dec 01 13:34:12 2011 +0100
@@ -16,7 +16,6 @@
sledgehammer_params [prover = e, blocking, timeout = 10, preplay_timeout = 0]
-
text {* Setup for testing Metis exhaustively *}
lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
@@ -83,7 +82,6 @@
(fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_encs))
*} "exhaustively run the new Metis with all type encodings"
-
text {* Miscellaneous tests *}
lemma "x = y \<Longrightarrow> y = x"