src/HOLCF/HOLCF.thy
changeset 15651 4b393520846e
parent 15650 b37dc98fbbc5
child 15742 64eae3513064
--- a/src/HOLCF/HOLCF.thy	Sat Apr 02 00:12:38 2005 +0200
+++ b/src/HOLCF/HOLCF.thy	Sat Apr 02 00:33:51 2005 +0200
@@ -9,4 +9,11 @@
 imports Sprod Ssum Up Lift Discrete One Tr
 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