# HG changeset patch
# User paulson
# Date 1102439413 -3600
# Node ID b13eb8a8897de7478a9ecf5b9131c213b49ea0cf
# Parent  c49e4225ef4f922bb20144c88240cad382592e7c
renamed attributes to lower case

diff -r c49e4225ef4f -r b13eb8a8897d src/HOL/Tools/reconstruction.ML
--- a/src/HOL/Tools/reconstruction.ML	Tue Dec 07 16:16:23 2004 +0100
+++ b/src/HOL/Tools/reconstruction.ML	Tue Dec 07 18:10:13 2004 +0100
@@ -50,13 +50,13 @@
 
 fun binary_syntax ((i, B), j) (x, A) = (x, binary_rule ((A,i), (B,j)));
 
-fun gen_BINARY thm = syntax
+fun gen_binary thm = syntax
       ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> binary_syntax);
-val BINARY_global = gen_BINARY global_thm;
-val BINARY_local = gen_BINARY local_thm;
+val binary_global = gen_binary global_thm;
+val binary_local = gen_binary local_thm;
 
 (*I have not done the MRR rule because it seems to be identifical to 
-BINARY*)
+binary*)
 
 
 fun inst_single sign t1 t2 cl =
@@ -92,7 +92,7 @@
 
 fun factor_syntax (i, j) (x, A) = (x, factor_rule (A,i,j));
 
-fun FACTOR x = syntax ((Scan.lift (Args.nat -- Args.nat)) >> factor_syntax) x;
+fun factor x = syntax ((Scan.lift (Args.nat -- Args.nat)) >> factor_syntax) x;
 
 
 (** Paramodulation **)
@@ -138,10 +138,10 @@
 
 fun paramod_syntax ((i, B), j) (x, A) = (x, paramod_rule ((A,i), (B,j)));
 
-fun gen_PARAMOD thm = syntax
+fun gen_paramod thm = syntax
       ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> paramod_syntax);
-val PARAMOD_global = gen_PARAMOD global_thm;
-val PARAMOD_local = gen_PARAMOD local_thm;
+val paramod_global = gen_paramod global_thm;
+val paramod_local = gen_paramod local_thm;
 
 
 (** Demodulation, i.e. rewriting **)
@@ -158,9 +158,9 @@
 
 fun demod_syntax (i, B) (x, A) = (x, demod_rule (A,i,B));
 
-fun gen_DEMOD thm = syntax ((Scan.lift Args.nat -- thm) >> demod_syntax);
-val DEMOD_global = gen_DEMOD global_thm;
-val DEMOD_local = gen_DEMOD local_thm;
+fun gen_demod thm = syntax ((Scan.lift Args.nat -- thm) >> demod_syntax);
+val demod_global = gen_demod global_thm;
+val demod_local = gen_demod local_thm;
 
 
 (** Conversion of a theorem into clauses **)
@@ -172,18 +172,18 @@
 
 fun clausify_syntax i (x, A) = (x, clausify_rule (A,i));
 
-fun CLAUSIFY x = syntax ((Scan.lift Args.nat) >> clausify_syntax) x;
+fun clausify x = syntax ((Scan.lift Args.nat) >> clausify_syntax) x;
 
 
 (** theory setup **)
 
 val setup =
   [Attrib.add_attributes
-     [("BINARY", (BINARY_global, BINARY_local), "binary resolution"),
-      ("PARAMOD", (PARAMOD_global, PARAMOD_local), "paramodulation"),
-      ("DEMOD", (DEMOD_global, DEMOD_local), "demodulation"),
-      ("FACTOR", (FACTOR, FACTOR), "factoring"),
-      ("CLAUSIFY", (CLAUSIFY, CLAUSIFY), "conversion to clauses")]];
+     [("binary", (binary_global, binary_local), "binary resolution"),
+      ("paramod", (paramod_global, paramod_local), "paramodulation"),
+      ("demod", (demod_global, demod_local), "demodulation"),
+      ("factor", (factor, factor), "factoring"),
+      ("clausify", (clausify, clausify), "conversion to clauses")]];
 
 end
 end
diff -r c49e4225ef4f -r b13eb8a8897d src/HOL/ex/Classical.thy
--- a/src/HOL/ex/Classical.thy	Tue Dec 07 16:16:23 2004 +0100
+++ b/src/HOL/ex/Classical.thy	Tue Dec 07 18:10:13 2004 +0100
@@ -720,8 +720,8 @@
        (\<forall>x. (P4 x|P5 x) --> (\<exists>y. Q0 y & R x y))
        --> (\<exists>x y. P0 x & P0 y & (\<exists>z. Q1 z & R y z & R x y))"
 by (tactic{*safe_best_meson_tac 1*})
-    --{*Considerably faster than @{text meson},
-        which does iterative deepening rather than best-first search*}
+    --{*Nearly twice as fast as @{text meson},
+        which performs iterative deepening rather than best-first search*}
 
 text{*The Los problem. Circulated by John Harrison*}
 lemma "(\<forall>x y z. P x y & P y z --> P x z) &
@@ -794,9 +794,9 @@
      and Q: "\<And>U. Q U \<Longrightarrow> False"
      and PQ: "\<And>U.  \<lbrakk>P (f U); \<not> Q (g U)\<rbrakk> \<Longrightarrow> False"
   have cl4: "\<And>U. \<not> Q (g U) \<Longrightarrow> False"
-    by (rule P [BINARY 0 PQ 0])
+    by (rule P [binary 0 PQ 0])
   show "False"
-    by (rule Q [BINARY 0 cl4 0])
+    by (rule Q [binary 0 cl4 0])
 qed
 
 end