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