src/HOLCF/HOLCF.thy
changeset 16054 b8ba6727712f
parent 15742 64eae3513064
child 16841 228d663cc9b3
--- a/src/HOLCF/HOLCF.thy	Mon May 23 23:01:27 2005 +0200
+++ b/src/HOLCF/HOLCF.thy	Mon May 23 23:24:38 2005 +0200
@@ -9,11 +9,4 @@
 imports Sprod Ssum Up Lift Discrete One Tr Domain
 begin
 
-text {*
-  Remove continuity lemmas from simp set, so continuity subgoals
-  are handled by the @{text cont_proc} simplifier procedure.
-*}
-declare cont_lemmas1 [simp del]
-declare cont_lemmas_ext [simp del]
-
 end