# HG changeset patch
# User nipkow
# Date 889013651 -3600
# Node ID c4b07b8579fdb8fd180b095febebdc6d36499ba8
# Parent  335dfafb18165f7b20d9b5c5a49dda935d39ddd2
Reorganized simplifier. May now reorient rules.

diff -r 335dfafb1816 -r c4b07b8579fd src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Mar 03 15:15:04 1998 +0100
+++ b/src/HOL/simpdata.ML	Wed Mar 04 13:14:11 1998 +0100
@@ -83,13 +83,11 @@
 in
 
   fun mk_meta_eq r = r RS eq_reflection;
+  fun mk_meta_eq_True r = Some(r RS meta_eq_to_obj_eq RS P_imp_P_eq_True);
 
   fun mk_meta_eq_simp r = case concl_of r of
           Const("==",_)$_$_ => r
-      |   _$(Const("op =",_)$lhs$rhs) =>
-             (case fst(Logic.rewrite_rule_ok (#sign(rep_thm r)) (prems_of r) lhs rhs) of
-                None => mk_meta_eq r
-              | Some _ => r RS P_imp_P_eq_True)
+      |   _$(Const("op =",_)$lhs$rhs) => mk_meta_eq r
       |   _$(Const("Not",_)$_) => r RS not_P_imp_P_eq_False
       |   _ => r RS P_imp_P_eq_True;
   (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
@@ -386,7 +384,8 @@
 val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
 			    setSSolver   safe_solver
 			    setSolver  unsafe_solver
-			    setmksimps (mksimps mksimps_pairs);
+			    setmksimps (mksimps mksimps_pairs)
+			    setmkeqTrue mk_meta_eq_True;
 
 val HOL_ss = 
     HOL_basic_ss addsimps 
diff -r 335dfafb1816 -r c4b07b8579fd src/HOLCF/ex/Focus_ex.ML
--- a/src/HOLCF/ex/Focus_ex.ML	Tue Mar 03 15:15:04 1998 +0100
+++ b/src/HOLCF/ex/Focus_ex.ML	Wed Mar 04 13:14:11 1998 +0100
@@ -100,7 +100,6 @@
 by (rtac sym 1);
 by (rtac fix_eqI 1);
 by (asm_simp_tac HOLCF_ss 1);
-by (etac sym 1);
 by (rtac allI 1);
 by (simp_tac HOLCF_ss 1);
 by (strip_tac 1);
diff -r 335dfafb1816 -r c4b07b8579fd src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Tue Mar 03 15:15:04 1998 +0100
+++ b/src/Provers/simplifier.ML	Wed Mar 04 13:14:11 1998 +0100
@@ -8,8 +8,8 @@
 
 infix 4
   setsubgoaler setloop addloop setSSolver addSSolver setSolver
-  addSolver setmksimps addsimps delsimps addeqcongs deleqcongs
-  settermless addsimprocs delsimprocs;
+  addSolver addsimps delsimps addeqcongs deleqcongs
+  setmksimps setmkeqTrue setmksym settermless addsimprocs delsimprocs;
 
 
 signature SIMPLIFIER =
@@ -35,6 +35,8 @@
   val setSolver:    simpset * (thm list -> int -> tactic) -> simpset
   val addSolver:    simpset * (thm list -> int -> tactic) -> simpset
   val setmksimps:   simpset * (thm -> thm list) -> simpset
+  val setmkeqTrue:  simpset * (thm -> thm option) -> simpset
+  val setmksym:     simpset * (thm -> thm option) -> simpset
   val settermless:  simpset * (term * term -> bool) -> simpset
   val addsimps:     simpset * thm list -> simpset
   val delsimps:     simpset * thm list -> simpset
@@ -111,7 +113,8 @@
     finish_tac = finish_tac, unsafe_finish_tac = unsafe_finish_tac};
 
 val empty_ss =
-  make_ss (Thm.empty_mss, K (K no_tac), [], K (K no_tac), K (K no_tac));
+  let val mss = Thm.set_mk_sym(Thm.empty_mss, Some o symmetric_fun)
+  in make_ss (mss, K (K no_tac), [], K (K no_tac), K (K no_tac)) end;
 
 fun rep_ss (Simpset args) = args;
 fun prems_of_ss (Simpset {mss, ...}) = Thm.prems_of_mss mss;
@@ -172,6 +175,16 @@
   make_ss (Thm.set_mk_rews (mss, map (Thm.strip_shyps o Drule.zero_var_indexes) o mk_simps),
     subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
 
+fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
+    setmkeqTrue mk_eq_True =
+  make_ss (Thm.set_mk_eq_True (mss, mk_eq_True),
+    subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
+
+fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
+    setmksym mksym =
+  make_ss (Thm.set_mk_sym (mss, mksym),
+    subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
+
 fun (Simpset {mss, subgoal_tac, loop_tacs,  finish_tac, unsafe_finish_tac})
     settermless termless =
   make_ss (Thm.set_termless (mss, termless), subgoal_tac, loop_tacs,