# HG changeset patch
# User huffman
# Date 1116883478 -7200
# Node ID b8ba6727712fd4d77df1b18f8c6acd7f3addb8a2
# Parent  603820cad0835b48773a77ca0760209722a397fc
moved continuity simproc to Cont.thy

diff -r 603820cad083 -r b8ba6727712f src/HOLCF/HOLCF.thy
--- 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
diff -r 603820cad083 -r b8ba6727712f src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Mon May 23 23:01:27 2005 +0200
+++ b/src/HOLCF/Lift.thy	Mon May 23 23:24:38 2005 +0200
@@ -293,11 +293,6 @@
   \medskip Extension of @{text cont_tac} and installation of simplifier.
 *}
 
-lemma cont2cont_CF1L_rev2: "(!!y. cont (%x. c1 x y)) ==> cont c1"
-  apply (rule cont2cont_CF1L_rev)
-  apply simp
-  done
-
 lemmas cont_lemmas_ext [simp] =
   cont_flift1_arg cont_flift2_arg
   cont_flift1_arg_and_not_arg cont2cont_CF1L_rev2
@@ -316,28 +311,6 @@
 end;
 *}
 
-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];
-*}
-
 
 subsection {* flift1, flift2 *}