diff -r 89669c58e506 -r 0bba840aa07c simpdata.ML
--- a/simpdata.ML	Thu Aug 25 11:01:45 1994 +0200
+++ b/simpdata.ML	Tue Aug 30 10:04:49 1994 +0200
@@ -18,20 +18,20 @@
 val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp;
 val not_P_imp_P_eq_False = not_P_imp_P_iff_F RS eq_reflection;
 
-fun atomize r =
-  case concl_of r of
-    Const("Trueprop",_) $ p =>
-      (case p of
-	 Const("op -->",_)$_$_ => atomize(r RS mp)
-       | Const("op &",_)$_$_ => atomize(r RS conjunct1) @
-	  		        atomize(r RS conjunct2)
-       | Const("All",_)$_ => atomize(r RS spec)
-       | Const("True",_) => []
-       | Const("False",_) => []
-       | _ => [r])
-  | _ => [r];
+fun atomize pairs =
+  let fun atoms th =
+        (case concl_of th of
+           Const("Trueprop",_) $ p =>
+             (case head_of p of
+                Const(a,_) =>
+                  (case assoc(pairs,a) of
+                     Some(rls) => flat (map atoms ([th] RL rls))
+                   | None => [th])
+              | _ => [th])
+         | _ => [th])
+  in atoms end;
 
-fun mk_eq r = case concl_of r of
+fun mk_meta_eq r = case concl_of r of
 	Const("==",_)$_$_ => r
     |	_$(Const("op =",_)$_$_) => r RS eq_reflection
     |	_$(Const("not",_)$_) => r RS not_P_imp_P_eq_False
@@ -40,8 +40,6 @@
 
 fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
 
-fun mk_rews thm = map mk_eq (atomize(gen_all thm));
-
 val imp_cong = impI RSN
     (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
 	(fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
@@ -56,6 +54,7 @@
    "(True=P) = P", "(P=True) = P",
    "(True --> P) = P", "(False --> P) = True", 
    "(P --> True) = True", "(P --> P) = True",
+   "(P --> False) = (~P)", "(P --> ~P) = (~P)",
    "(P & True) = P", "(True & P) = P", 
    "(P & False) = False", "(False & P) = False", "(P & P) = P",
    "(P | True) = True", "(True | P) = True", 
@@ -97,8 +96,14 @@
 infix addcongs;
 fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);
 
+val mksimps_pairs =
+  [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
+   ("All", [spec]), ("True", []), ("False", [])];
+
+fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all;
+
 val HOL_ss = empty_ss
-      setmksimps mk_rews
+      setmksimps (mksimps mksimps_pairs)
       setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
                              ORELSE' etac FalseE)
       setsubgoaler asm_simp_tac
@@ -106,7 +111,7 @@
       addcongs [imp_cong];
 
 fun split_tac splits =
-  mk_case_split_tac (meta_eq_to_obj_eq RS iffD2) (map mk_eq splits);
+  mk_case_split_tac (meta_eq_to_obj_eq RS iffD2) (map mk_meta_eq splits);
 
 (* eliminiation of existential quantifiers in assumptions *)