--- 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"
--- 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 *}
--- 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);
--- 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,
--- 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 *)
--- 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 *)