author | blanchet |
Tue, 09 Sep 2014 20:51:36 +0200 | |
changeset 58276 | aa1b6ea6a893 |
parent 58275 | 280ede57a6a9 |
child 58277 | 0dcd3a623a6e |
--- 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