# HG changeset patch
# User huffman
# Date 1112394831 -7200
# Node ID 4b393520846e3b88b796999fc7f6963834791180
# Parent  b37dc98fbbc536d08345fdcd3c43d02c7667286c
Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used.

diff -r b37dc98fbbc5 -r 4b393520846e src/HOLCF/HOLCF.thy
--- 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
diff -r b37dc98fbbc5 -r 4b393520846e src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Sat Apr 02 00:12:38 2005 +0200
+++ b/src/HOLCF/Lift.thy	Sat Apr 02 00:33:51 2005 +0200
@@ -314,9 +314,28 @@
   simp_tac (simpset() addsimps [flift1_def, flift2_def]) i THEN
   REPEAT (cont_tac i)
 end;
+*}
 
-simpset_ref() := simpset() addSolver
-  (mk_solver "cont_tac" (K (DEPTH_SOLVE_1 o cont_tac)));
+text {*
+  New continuity simproc by Brian Huffman.
+  Given the term @{term "cont f"}, the procedure tries to
+  construct the theorem @{prop "cont f == True"}. If this
+  theorem cannot be completely solved by the introduction
+  rules, then the procedure returns a conditional rewrite
+  rule with the unsolved subgoals as premises.
+*}
+
+ML_setup {*
+local fun solve_cont sg _ t = let
+  val tr = instantiate' [] [SOME (cterm_of sg t)] Eq_TrueI
+  val tac = REPEAT_ALL_NEW cont_tac 1
+  in Option.map fst (Seq.pull (tac tr))
+  end;
+
+in val cont_proc = Simplifier.simproc (Theory.sign_of (the_context ()))
+         "continuity" ["cont f"] solve_cont;
+end;
+Addsimprocs [cont_proc];
 *}