# HG changeset patch
# User nipkow
# Date 880699284 -3600
# Node ID 2a2956ccb86c8936b0a130a1b189caeee375b18f
# Parent  24d9e6639cd4bf080f311d4d3e35d7b8b4421198
Removed dead code.

diff -r 24d9e6639cd4 -r 2a2956ccb86c src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Nov 28 07:37:06 1997 +0100
+++ b/src/HOL/simpdata.ML	Fri Nov 28 07:41:24 1997 +0100
@@ -170,91 +170,6 @@
                  "(ALL x. P x --> Q) = ((EX x. P x) --> Q)",
                  "(ALL x. P --> Q x) = (P --> (ALL x. Q x))"];
 
-(*** Simplification procedures for turning
-
-            ? x. ... & x = t & ...
-     into   ? x. x = t & ... & ...
-     where the `? x. x = t &' in the latter formula is eliminated
-           by ordinary simplification. 
-
-     and   ! x. (... & x = t & ...) --> P x
-     into  ! x. x = t --> (... & ...) --> P x
-     where the `!x. x=t -->' in the latter formula is eliminated
-           by ordinary simplification.
-
-NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)"
-   "!x. x=t --> P(x)" and "!x. t=x --> P(x)"
-   must be taken care of by ordinary rewrite rules.
-
-local
-
-fun def(eq as (c as Const("op =",_)) $ s $ t) =
-      if s = Bound 0 andalso not(loose_bvar1(t,0)) then Some eq else
-      if t = Bound 0 andalso not(loose_bvar1(s,0)) then Some(c$t$s)
-      else None
-  | def _ = None;
-
-fun extract(Const("op &",_) $ P $ Q) =
-      (case def P of
-         Some eq => Some(eq,Q)
-       | None => (case def Q of
-                   Some eq => Some(eq,P)
-                 | None =>
-       (case extract P of
-         Some(eq,P') => Some(eq, HOLogic.conj $ P' $ Q)
-       | None => (case extract Q of
-                   Some(eq,Q') => Some(eq,HOLogic.conj $ P $ Q')
-                 | None => None))))
-  | extract _ = None;
-
-fun prove_ex_eq(ceqt) =
-  let val tac = rtac eq_reflection 1 THEN rtac iffI 1 THEN
-                ALLGOALS(EVERY'[etac exE, REPEAT o (etac conjE),
-                 rtac exI, REPEAT o (ares_tac [conjI] ORELSE' etac sym)])
-  in rule_by_tactic tac (trivial ceqt) end;
-
-fun rearrange_ex sg _ (F as ex $ Abs(x,T,P)) =
-     (case extract P of
-        None => None
-      | Some(eq,Q) =>
-          let val ceqt = cterm_of sg
-                       (Logic.mk_equals(F,ex $ Abs(x,T,HOLogic.conj$eq$Q)))
-          in Some(prove_ex_eq ceqt) end)
-  | rearrange_ex _ _ _ = None;
-
-val ex_pattern =
-  read_cterm (sign_of HOL.thy) ("? x. P(x) & Q(x)",HOLogic.boolT)
-
-fun prove_all_eq(ceqt) =
-  let fun tac _ = [EVERY1[rtac eq_reflection, rtac iffI,
-                       rtac allI, etac allE, rtac impI, rtac impI, etac mp,
-                          REPEAT o (etac conjE),
-                          REPEAT o (ares_tac [conjI] ORELSE' etac sym),
-                       rtac allI, etac allE, rtac impI, REPEAT o (etac conjE),
-                          etac impE, atac ORELSE' etac sym, etac mp,
-                          REPEAT o (ares_tac [conjI])]]
-  in prove_goalw_cterm [] ceqt tac end;
-
-fun rearrange_all sg _ (F as all $ Abs(x,T,Const("op -->",_)$P$Q)) =
-     (case extract P of
-        None => None
-      | Some(eq,P') =>
-          let val R = HOLogic.imp $ eq $ (HOLogic.imp $ P' $ Q)
-              val ceqt = cterm_of sg (Logic.mk_equals(F,all$Abs(x,T,R)))
-          in Some(prove_all_eq ceqt) end)
-  | rearrange_all _ _ _ = None;
-
-val all_pattern =
-  read_cterm (sign_of HOL.thy) ("! x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
-
-in
-val defEX_regroup = mk_simproc "defined EX" [ex_pattern] rearrange_ex;
-val defALL_regroup = mk_simproc "defined ALL" [all_pattern] rearrange_all;
-end;
-***)
-
-
-
 
 (* elimination of existential quantifiers in assumptions *)