# HG changeset patch
# User wenzelm
# Date 1007517965 -3600
# Node ID 80ca9058db95693a03a8502066541e0739b43d2f
# Parent  f9e6af324d35a721d2cb03505edfc4030f05bb70
tuned;

diff -r f9e6af324d35 -r 80ca9058db95 src/FOL/ex/Natural_Numbers.thy
--- a/src/FOL/ex/Natural_Numbers.thy	Wed Dec 05 03:05:39 2001 +0100
+++ b/src/FOL/ex/Natural_Numbers.thy	Wed Dec 05 03:06:05 2001 +0100
@@ -1,13 +1,18 @@
 (*  Title:      FOL/ex/Natural_Numbers.thy
     ID:         $Id$
     Author:     Markus Wenzel, TU Munich
-
-Theory of the natural numbers: Peano's axioms, primitive recursion.
-(Modernized version of Larry Paulson's theory "Nat".)
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
+header {* Natural numbers *}
+
 theory Natural_Numbers = FOL:
 
+text {*
+  Theory of the natural numbers: Peano's axioms, primitive recursion.
+  (Modernized version of Larry Paulson's theory "Nat".)  \medskip
+*}
+
 typedecl nat
 arities nat :: "term"
 
diff -r f9e6af324d35 -r 80ca9058db95 src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Wed Dec 05 03:05:39 2001 +0100
+++ b/src/HOL/Library/Quotient.thy	Wed Dec 05 03:06:05 2001 +0100
@@ -30,9 +30,9 @@
 axclass equiv \<subseteq> eqv
   equiv_refl [intro]: "x \<sim> x"
   equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
-  equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
+  equiv_sym [sym]: "x \<sim> y ==> y \<sim> x"
 
-lemma not_equiv_sym [elim?]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
+lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
 proof -
   assume "\<not> (x \<sim> y)" thus "\<not> (y \<sim> x)"
     by (rule contrapos_nn) (rule equiv_sym)
@@ -99,7 +99,7 @@
  relation.
 *}
 
-theorem quot_equality: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
+theorem quot_equality [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
 proof
   assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
   show "a \<sim> b"
@@ -132,18 +132,6 @@
   qed
 qed
 
-lemma quot_equalI [intro?]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
-  by (simp only: quot_equality)
-
-lemma quot_equalD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> b"
-  by (simp only: quot_equality)
-
-lemma quot_not_equalI [intro?]: "\<not> (a \<sim> b) ==> \<lfloor>a\<rfloor> \<noteq> \<lfloor>b\<rfloor>"
-  by (simp add: quot_equality)
-
-lemma quot_not_equalD [dest?]: "\<lfloor>a\<rfloor> \<noteq> \<lfloor>b\<rfloor> ==> \<not> (a \<sim> b)"
-  by (simp add: quot_equality)
-
 
 subsection {* Picking representing elements *}
 
diff -r f9e6af324d35 -r 80ca9058db95 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Wed Dec 05 03:05:39 2001 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Wed Dec 05 03:06:05 2001 +0100
@@ -170,12 +170,12 @@
 
 in
 
-val (simp_add_global, simp_add_local) = global_local map_simps (Drule.add_rules o single);
-val (simp_del_global, simp_del_local) = global_local map_simps (Drule.del_rules o single);
+val (simp_add_global, simp_add_local) = global_local map_simps Drule.add_rule;
+val (simp_del_global, simp_del_local) = global_local map_simps Drule.del_rule;
 val (cong_add_global, cong_add_local) = global_local map_congs add_cong;
 val (cong_del_global, cong_del_local) = global_local map_congs del_cong;
-val (wf_add_global, wf_add_local) = global_local map_wfs (Drule.add_rules o single);
-val (wf_del_global, wf_del_local) = global_local map_wfs (Drule.del_rules o single);
+val (wf_add_global, wf_add_local) = global_local map_wfs Drule.add_rule;
+val (wf_del_global, wf_del_local) = global_local map_wfs Drule.del_rule;
 
 val simp_attr = mk_attr (simp_add_global, simp_add_local) (simp_del_global, simp_del_local);
 val cong_attr = mk_attr (cong_add_global, cong_add_local) (cong_del_global, cong_del_local);
diff -r f9e6af324d35 -r 80ca9058db95 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Wed Dec 05 03:05:39 2001 +0100
+++ b/src/Provers/blast.ML	Wed Dec 05 03:06:05 2001 +0100
@@ -62,7 +62,6 @@
   val rep_cs	: (* dependent on classical.ML *)
       claset -> {safeIs: thm list, safeEs: thm list, 
 		 hazIs: thm list, hazEs: thm list,
-		 xtraIs: thm list, xtraEs: thm list,
 		 swrappers: (string * wrapper) list, 
 		 uwrappers: (string * wrapper) list,
 		 safe0_netpair: netpair, safep_netpair: netpair,
diff -r f9e6af324d35 -r 80ca9058db95 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Wed Dec 05 03:05:39 2001 +0100
+++ b/src/Pure/Isar/object_logic.ML	Wed Dec 05 03:06:05 2001 +0100
@@ -111,11 +111,11 @@
 val get_atomize = #1 o #2 o ObjectLogicData.get_sg;
 val get_rulify = #2 o #2 o ObjectLogicData.get_sg;
 
-val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rules;
-val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rules;
+val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rule;
+val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rule;
 
-fun declare_atomize (thy, th) = (add_atomize [th] thy, th);
-fun declare_rulify (thy, th) = (add_rulify [th] thy, th);
+fun declare_atomize (thy, th) = (add_atomize th thy, th);
+fun declare_rulify (thy, th) = (add_rulify th thy, th);
 
 
 (* atomize *)
diff -r f9e6af324d35 -r 80ca9058db95 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Dec 05 03:05:39 2001 +0100
+++ b/src/Pure/axclass.ML	Wed Dec 05 03:06:05 2001 +0100
@@ -320,7 +320,7 @@
   HEADGOAL (Method.some_rule_tac rules ctxt facts ORELSE' default_intro_classes_tac facts);
 
 val default_method =
-  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some rule")
+  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule");
 
 
 (* axclass_tac *)