removed debugging junk
authorblanchet
Tue, 09 Sep 2014 20:51:36 +0200
changeset 58276 aa1b6ea6a893
parent 58275 280ede57a6a9
child 58277 0dcd3a623a6e
removed debugging junk
src/HOL/BNF_Least_Fixpoint.thy
--- a/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -16,9 +16,6 @@
   "datatype_compat" :: thy_decl
 begin
 
-ML {* proofs := 2 *} (*###*)
-ML {* Proofterm.proofs_enabled () *}
-
 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
   by blast