# HG changeset patch
# User paulson
# Date 825504450 -3600
# Node ID 524879632d88140c5a448602aa57cd126533e4c8
# Parent  7513fbe502fb7170b0a7fa078cf3453ab1240fe5
imp_elim and swap are now stored in thm database

diff -r 7513fbe502fb -r 524879632d88 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Feb 28 11:46:08 1996 +0100
+++ b/src/Provers/classical.ML	Wed Feb 28 11:47:30 1996 +0100
@@ -90,7 +90,8 @@
 
 (** Useful tactics for classical reasoning **)
 
-val imp_elim = make_elim mp;
+val imp_elim = (*cannot use bind_thm within a structure!*)
+  store_thm ("imp_elim", make_elim mp);
 
 (*Solve goal that assumes both P and ~P. *)
 val contr_tac = eresolve_tac [not_elim]  THEN'  assume_tac;
@@ -102,7 +103,8 @@
 (*Like mp_tac but instantiates no variables*)
 fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i  THEN  eq_assume_tac i;
 
-val swap = rule_by_tactic (etac thin_rl 1) (not_elim RS classical);
+val swap =
+  store_thm ("swap", rule_by_tactic (etac thin_rl 1) (not_elim RS classical));
 
 (*Creates rules to eliminate ~A, from rules to introduce A*)
 fun swapify intrs = intrs RLN (2, [swap]);