Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simp del -> code del
authorhuffman
Mon, 01 Jun 2009 10:56:31 -0700
changeset 31356 ec8b9b6c47dc
parent 31355 3d18766ddc4b
child 31357 df6acdd9dd37
simp del -> code del
src/HOL/Limits.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Limits.thy	Mon Jun 01 10:36:42 2009 -0700
+++ b/src/HOL/Limits.thy	Mon Jun 01 10:56:31 2009 -0700
@@ -20,7 +20,7 @@
 
 definition
   eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool" where
-  [simp del]: "eventually P F \<longleftrightarrow> Rep_filter F P"
+  [code del]: "eventually P F \<longleftrightarrow> Rep_filter F P"
 
 lemma eventually_True [simp]: "eventually (\<lambda>x. True) F"
 unfolding eventually_def using Rep_filter [of F] by blast
isabelle