# HG changeset patch
# User wenzelm
# Date 1154000580 -7200
# Node ID 89d2758ecddf6dc041bcb4fea7a9241bd0e70656
# Parent  e2b876cd9e2925be0fdc1dc44b6fd7fb6abde42e
tuned proofs;

diff -r e2b876cd9e29 -r 89d2758ecddf src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Thu Jul 27 13:42:59 2006 +0200
+++ b/src/FOL/FOL.thy	Thu Jul 27 13:43:00 2006 +0200
@@ -34,9 +34,17 @@
 lemma ex1_functional: "[| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
 by blast
 
-ML {*
-val ex1_functional = thm "ex1_functional";
-*}
+ML {* val ex1_functional = thm "ex1_functional" *}
+
+(* Elimination of True from asumptions: *)
+lemma True_implies_equals: "(True ==> PROP P) == PROP P"
+proof
+  assume "True \<Longrightarrow> PROP P"
+  from this and TrueI show "PROP P" .
+next
+  assume "PROP P"
+  then show "PROP P" .
+qed
 
 use "simpdata.ML"
 setup simpsetup
diff -r e2b876cd9e29 -r 89d2758ecddf src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Thu Jul 27 13:42:59 2006 +0200
+++ b/src/FOL/simpdata.ML	Thu Jul 27 13:43:00 2006 +0200
@@ -6,14 +6,9 @@
 Simplification data for FOL.
 *)
 
-
-(* Elimination of True from asumptions: *)
+val ex1_functional = thm "ex1_functional";
+val True_implies_equals = thm "True_implies_equals";
 
-bind_thm ("True_implies_equals", prove_goal IFOL.thy
- "(True ==> PROP P) == PROP P"
-(K [rtac equal_intr_rule 1, atac 2,
-          METAHYPS (fn prems => resolve_tac prems 1) 1,
-          rtac TrueI 1]));
 
 
 (*** Rewrite rules ***)
diff -r e2b876cd9e29 -r 89d2758ecddf src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Jul 27 13:42:59 2006 +0200
+++ b/src/HOL/HOL.thy	Thu Jul 27 13:43:00 2006 +0200
@@ -914,14 +914,15 @@
 
 use "cladata.ML"
 setup hypsubst_setup
-
 setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) *}
-
 setup Classical.setup
+setup ResAtpSet.setup
+setup clasetup
 
-setup ResAtpSet.setup
-
-setup clasetup
+lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
+  apply (erule swap)
+  apply (erule (1) meta_mp)
+  done
 
 declare ex_ex1I [rule del, intro! 2]
   and ex1I [intro]
diff -r e2b876cd9e29 -r 89d2758ecddf src/HOL/TLA/TLA.ML
--- a/src/HOL/TLA/TLA.ML	Thu Jul 27 13:42:59 2006 +0200
+++ b/src/HOL/TLA/TLA.ML	Thu Jul 27 13:43:00 2006 +0200
@@ -243,6 +243,7 @@
 *)
 bind_thm("all_box", standard((temp_unlift allT) RS sym));
 
+bind_thm ("contrapos_np", thm "contrapos_np");
 
 Goal "|- (<>(F | G)) = (<>F | <>G)";
 by (auto_tac (temp_css addsimps2 [dmd_def,split_box_conj]));
diff -r e2b876cd9e29 -r 89d2758ecddf src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Thu Jul 27 13:42:59 2006 +0200
+++ b/src/HOL/cladata.ML	Thu Jul 27 13:43:00 2006 +0200
@@ -52,8 +52,6 @@
 
 open BasicClassical;
 
-val _ = bind_thm ("contrapos_np", inst "Pa" "?Q" Classical.swap);
-
 (*Propositional rules*)
 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
                        addSEs [conjE,disjE,impCE,FalseE,iffCE];