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