# HG changeset patch # User huffman # Date 1241128019 25200 # Node ID 5ee6368d622bdbc6ee577e0c33625667ee774886 # Parent e564767f8f78066b1066460106ea7f6e37048dc6 use simproc_setup command for cont_proc diff -r e564767f8f78 -r 5ee6368d622b src/HOLCF/Cont.thy --- a/src/HOLCF/Cont.thy Thu Apr 30 12:16:35 2009 -0700 +++ b/src/HOLCF/Cont.thy Thu Apr 30 14:46:59 2009 -0700 @@ -144,7 +144,7 @@ ( val name = "cont2cont" val description = "continuity intro rule" ) *} -setup {* Cont2ContData.setup *} +setup Cont2ContData.setup text {* Given the term @{term "cont f"}, the procedure tries to construct the @@ -153,20 +153,13 @@ conditional rewrite rule with the unsolved subgoals as premises. *} -setup {* -let - fun solve_cont thy ss t = +simproc_setup cont_proc ("cont f") = {* + fn phi => fn ss => fn ct => let - val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI; + val tr = instantiate' [] [SOME ct] @{thm Eq_TrueI}; val rules = Cont2ContData.get (Simplifier.the_context ss); val tac = REPEAT_ALL_NEW (match_tac rules); - in Option.map fst (Seq.pull (tac 1 tr)) end - - val proc = - Simplifier.simproc @{theory} "cont_proc" ["cont f"] solve_cont; -in - Simplifier.map_simpset (fn ss => ss addsimprocs [proc]) -end + in SINGLE (tac 1) tr end *} subsection {* Continuity of basic functions *}