# HG changeset patch
# User wenzelm
# Date 1112858733 -7200
# Node ID 9ef583b0864742b2562f5a8c9c85c6b19960a82b
# Parent  255055554c6750b8fe22ad65f5df4a006b10bb46
reverted renaming of Some/None in comments and strings;

diff -r 255055554c67 -r 9ef583b08647 Admin/Benchmarks/HOL-datatype/ROOT.ML
--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Admin/Benchmarks/HOL-datatype/ROOT.ML
     ID:         $Id$
 
-SOME rather large datatype examples (from John Harrison).
+Some rather large datatype examples (from John Harrison).
 *)
 
 val tests = ["Brackin", "Instructions", "SML", "Verilog"];
diff -r 255055554c67 -r 9ef583b08647 src/CTT/ex/elim.ML
--- a/src/CTT/ex/elim.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/CTT/ex/elim.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-SOME examples taken from P. Martin-L\"of, Intuitionistic type theory
+Some examples taken from P. Martin-L\"of, Intuitionistic type theory
         (Bibliopolis, 1984).
 
 by (safe_tac prems 1);
diff -r 255055554c67 -r 9ef583b08647 src/Cube/ex/ex.ML
--- a/src/Cube/ex/ex.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/Cube/ex/ex.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -201,7 +201,7 @@
 by (EVERY[etac pi_elim 1, assume_tac 1, assume_tac 1]);
 uresult();
 
-(* SOME random examples *)
+(* Some random examples *)
 
 goal LP2.thy "A:* c:A f:A->A |- \
 \       Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";
diff -r 255055554c67 -r 9ef583b08647 src/FOL/IFOL_lemmas.ML
--- a/src/FOL/IFOL_lemmas.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/FOL/IFOL_lemmas.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -204,7 +204,7 @@
 by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ;
 qed "ex1I";
 
-(*SOMEtimes easier to use: the premises have no shared variables.  Safe!*)
+(*Sometimes easier to use: the premises have no shared variables.  Safe!*)
 val [ex,eq] = Goal
     "[| EX x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)";
 by (rtac (ex RS exE) 1);
diff -r 255055554c67 -r 9ef583b08647 src/FOL/ex/int.ML
--- a/src/FOL/ex/int.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/FOL/ex/int.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -296,7 +296,7 @@
 writeln"Hard examples with quantifiers";
 
 (*The ones that have not been proved are not known to be valid!
-  SOME will require quantifier duplication -- not currently available*)
+  Some will require quantifier duplication -- not currently available*)
 
 writeln"Problem ~~18";
 Goal "~~(EX y. ALL x. P(y)-->P(x))";
diff -r 255055554c67 -r 9ef583b08647 src/FOL/ex/intro.ML
--- a/src/FOL/ex/intro.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/FOL/ex/intro.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -14,7 +14,7 @@
 
 context FOL.thy;
 
-(**** SOME simple backward proofs ****)
+(**** Some simple backward proofs ****)
 
 Goal "P|P --> P";
 by (rtac impI 1);
diff -r 255055554c67 -r 9ef583b08647 src/FOL/ex/quant.ML
--- a/src/FOL/ex/quant.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/FOL/ex/quant.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -34,7 +34,7 @@
 result();  
 
 
-writeln"SOME harder ones";
+writeln"Some harder ones";
 
 Goal "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
 by tac;
@@ -104,7 +104,7 @@
 result();  
 
 
-writeln"SOME slow ones";
+writeln"Some slow ones";
 
 
 (*Principia Mathematica *11.53  *)
diff -r 255055554c67 -r 9ef583b08647 src/FOLP/ex/int.ML
--- a/src/FOLP/ex/int.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/FOLP/ex/int.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -231,7 +231,7 @@
 writeln"Hard examples with quantifiers";
 
 (*The ones that have not been proved are not known to be valid!
-  SOME will require quantifier duplication -- not currently available*)
+  Some will require quantifier duplication -- not currently available*)
 
 writeln"Problem ~~18";
 goal IFOLP.thy "?p : ~~(EX y. ALL x. P(y)-->P(x))";
diff -r 255055554c67 -r 9ef583b08647 src/FOLP/ex/intro.ML
--- a/src/FOLP/ex/intro.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/FOLP/ex/intro.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -12,7 +12,7 @@
 *)
 
 
-(**** SOME simple backward proofs ****)
+(**** Some simple backward proofs ****)
 
 goal FOLP.thy "?p:P|P --> P";
 by (rtac impI 1);
diff -r 255055554c67 -r 9ef583b08647 src/FOLP/ex/quant.ML
--- a/src/FOLP/ex/quant.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/FOLP/ex/quant.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -34,7 +34,7 @@
 result();  
 
 
-writeln"SOME harder ones";
+writeln"Some harder ones";
 
 Goal "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
 by tac;
@@ -104,7 +104,7 @@
 result();  
 
 
-writeln"SOME slow ones";
+writeln"Some slow ones";
 
 
 (*Principia Mathematica *11.53  *)
diff -r 255055554c67 -r 9ef583b08647 src/HOL/Algebra/abstract/order.ML
--- a/src/HOL/Algebra/abstract/order.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/Algebra/abstract/order.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -60,7 +60,7 @@
 
 fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);
 
-(* SOME code useful for debugging
+(* Some code useful for debugging
 
 val intT = HOLogic.intT;
 val a = Free ("a", intT);
diff -r 255055554c67 -r 9ef583b08647 src/HOL/Hoare/hoare.ML
--- a/src/HOL/Hoare/hoare.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/Hoare/hoare.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -89,7 +89,7 @@
 
 (*****************************************************************************)
 (** Simplifying:                                                            **)
-(** SOME useful lemmata, lists and simplification tactics to control which  **)
+(** Some useful lemmata, lists and simplification tactics to control which  **)
 (** theorems are used to simplify at each moment, so that the original      **)
 (** input does not suffer any unexpected transformation                     **)
 (*****************************************************************************)
diff -r 255055554c67 -r 9ef583b08647 src/HOL/Hoare/hoareAbort.ML
--- a/src/HOL/Hoare/hoareAbort.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/Hoare/hoareAbort.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -90,7 +90,7 @@
 
 (*****************************************************************************)
 (** Simplifying:                                                            **)
-(** SOME useful lemmata, lists and simplification tactics to control which  **)
+(** Some useful lemmata, lists and simplification tactics to control which  **)
 (** theorems are used to simplify at each moment, so that the original      **)
 (** input does not suffer any unexpected transformation                     **)
 (*****************************************************************************)
diff -r 255055554c67 -r 9ef583b08647 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/Import/shuffler.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -304,7 +304,7 @@
 		val lhs = #1 (Logic.dest_equals (prop_of (final init)))
 	    in
 		if not (lhs aconv origt)
-		then (writeln "SOMEthing is utterly wrong: (orig,lhs,frozen type,t,tinst)";
+		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
 		      writeln (string_of_cterm (cterm_of sg origt));
 		      writeln (string_of_cterm (cterm_of sg lhs));
 		      writeln (string_of_cterm (cterm_of sg typet));
@@ -359,7 +359,7 @@
 		val lhs = #1 (Logic.dest_equals (prop_of (final init)))
 	    in
 		if not (lhs aconv origt)
-		then (writeln "SOMEthing is utterly wrong: (orig,lhs,frozen type,t,tinst)";
+		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
 		      writeln (string_of_cterm (cterm_of sg origt));
 		      writeln (string_of_cterm (cterm_of sg lhs));
 		      writeln (string_of_cterm (cterm_of sg typet));
diff -r 255055554c67 -r 9ef583b08647 src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/Integ/cooper_dec.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -92,7 +92,7 @@
 fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
    |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
    |dest_numeral (Const ("Numeral.number_of",_) $ n)= HOLogic.dest_binum n; 
-(*SOME terms often used for pattern matching*) 
+(*Some terms often used for pattern matching*) 
  
 val zero = mk_numeral 0; 
 val one = mk_numeral 1; 
diff -r 255055554c67 -r 9ef583b08647 src/HOL/Integ/cooper_proof.ML
--- a/src/HOL/Integ/cooper_proof.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/Integ/cooper_proof.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -380,7 +380,7 @@
 (*==================================================*)
 fun rho_for_modd_minf x dlcm sg fm1 =
 let
-    (*SOME certified Terms*)
+    (*Some certified Terms*)
     
    val ctrue = cterm_of sg HOLogic.true_const
    val cfalse = cterm_of sg HOLogic.false_const
@@ -476,7 +476,7 @@
 (* -------------------------------------------------------------*)
 fun rho_for_modd_pinf x dlcm sg fm1 = 
 let
-    (*SOME certified Terms*)
+    (*Some certified Terms*)
     
   val ctrue = cterm_of sg HOLogic.true_const
   val cfalse = cterm_of sg HOLogic.false_const
diff -r 255055554c67 -r 9ef583b08647 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -538,7 +538,7 @@
 Addsimprocs [fast_int_arith_simproc]
 
 
-(* SOME test data
+(* Some test data
 Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
 by (fast_arith_tac 1);
 Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)";
diff -r 255055554c67 -r 9ef583b08647 src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/Integ/presburger.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -73,7 +73,7 @@
 
 fun term_typed_consts t = add_term_typed_consts(t,[]);
 
-(* SOME Types*)
+(* Some Types*)
 val bT = HOLogic.boolT;
 val bitT = HOLogic.bitT;
 val iT = HOLogic.intT;
@@ -249,7 +249,7 @@
     val g' = if a then abstract_pres sg g else g
     (* Transform the term*)
     val (t,np,nh) = prepare_for_presburger sg q g'
-    (* SOME simpsets for dealing with mod div abs and nat*)
+    (* Some simpsets for dealing with mod div abs and nat*)
     val simpset0 = HOL_basic_ss
       addsimps [mod_div_equality', Suc_plus1]
       addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
diff -r 255055554c67 -r 9ef583b08647 src/HOL/Real/real_arith.ML
--- a/src/HOL/Real/real_arith.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/Real/real_arith.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -136,7 +136,7 @@
 end;
 
 
-(* SOME test data [omitting examples that assume the ordering to be discrete!]
+(* Some test data [omitting examples that assume the ordering to be discrete!]
 Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
 by (fast_arith_tac 1);
 qed "";
diff -r 255055554c67 -r 9ef583b08647 src/HOL/TLA/TLA.ML
--- a/src/HOL/TLA/TLA.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/TLA/TLA.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -818,7 +818,7 @@
 by (asm_simp_tac (simpset() addsimps [split_box_conj,box_stp_actI]) 1);
 qed "WF1";
 
-(* SOMEtimes easier to use; designed for action B rather than state predicate Q *)
+(* Sometimes easier to use; designed for action B rather than state predicate Q *)
 val [prem1,prem2,prem3] = goalw thy [leadsto_def]
   "[| |- N & $P --> $Enabled (<A>_v);            \
 \     |- N & <A>_v --> B;                  \ 
diff -r 255055554c67 -r 9ef583b08647 src/HOL/Tools/Presburger/cooper_dec.ML
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -92,7 +92,7 @@
 fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
    |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
    |dest_numeral (Const ("Numeral.number_of",_) $ n)= HOLogic.dest_binum n; 
-(*SOME terms often used for pattern matching*) 
+(*Some terms often used for pattern matching*) 
  
 val zero = mk_numeral 0; 
 val one = mk_numeral 1; 
diff -r 255055554c67 -r 9ef583b08647 src/HOL/Tools/Presburger/cooper_proof.ML
--- a/src/HOL/Tools/Presburger/cooper_proof.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -380,7 +380,7 @@
 (*==================================================*)
 fun rho_for_modd_minf x dlcm sg fm1 =
 let
-    (*SOME certified Terms*)
+    (*Some certified Terms*)
     
    val ctrue = cterm_of sg HOLogic.true_const
    val cfalse = cterm_of sg HOLogic.false_const
@@ -476,7 +476,7 @@
 (* -------------------------------------------------------------*)
 fun rho_for_modd_pinf x dlcm sg fm1 = 
 let
-    (*SOME certified Terms*)
+    (*Some certified Terms*)
     
   val ctrue = cterm_of sg HOLogic.true_const
   val cfalse = cterm_of sg HOLogic.false_const
diff -r 255055554c67 -r 9ef583b08647 src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -73,7 +73,7 @@
 
 fun term_typed_consts t = add_term_typed_consts(t,[]);
 
-(* SOME Types*)
+(* Some Types*)
 val bT = HOLogic.boolT;
 val bitT = HOLogic.bitT;
 val iT = HOLogic.intT;
@@ -249,7 +249,7 @@
     val g' = if a then abstract_pres sg g else g
     (* Transform the term*)
     val (t,np,nh) = prepare_for_presburger sg q g'
-    (* SOME simpsets for dealing with mod div abs and nat*)
+    (* Some simpsets for dealing with mod div abs and nat*)
     val simpset0 = HOL_basic_ss
       addsimps [mod_div_equality', Suc_plus1]
       addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
diff -r 255055554c67 -r 9ef583b08647 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -945,7 +945,7 @@
     val dt_info = get_datatypes thy;
     val (descr, _) = unfold_datatypes sign dts' sorts dt_info dts' i;
     val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
-      if err then error ("NONEmptiness check failed for datatype " ^ s)
+      if err then error ("Nonemptiness check failed for datatype " ^ s)
       else raise exn;
 
     val descr' = List.concat descr;
diff -r 255055554c67 -r 9ef583b08647 src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/Tools/split_rule.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen
 
-SOME tools for managing tupled arguments and abstractions in rules.
+Some tools for managing tupled arguments and abstractions in rules.
 *)
 
 signature BASIC_SPLIT_RULE =
@@ -130,6 +130,8 @@
 
 (* attribute syntax *)
 
+(* FIXME dynamically scoped due to Args.name/pair_tac *)
+
 fun split_format x = Attrib.syntax
   (Scan.lift (Args.parens (Args.$$$ "complete"))
     >> K (Drule.rule_attribute (K complete_split_rule)) ||
diff -r 255055554c67 -r 9ef583b08647 src/HOL/ex/mesontest2.ML
--- a/src/HOL/ex/mesontest2.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/ex/mesontest2.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -193,7 +193,7 @@
 (*
  * Original timings for John Harrison's MESON_TAC.
  * Timings below on a 600MHz Pentium III (perch)
- * SOME timings below refer to griffon, which is a dual 2.5GHz Power Mac G5.
+ * Some timings below refer to griffon, which is a dual 2.5GHz Power Mac G5.
  * 
  * A few variable names have been changed to avoid clashing with constants.
  *
diff -r 255055554c67 -r 9ef583b08647 src/HOL/ex/svc_test.ML
--- a/src/HOL/ex/svc_test.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/ex/svc_test.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -18,7 +18,7 @@
 by (svc_tac 1);
 qed "";
 
-(** SOME big tautologies supplied by John Harrison **)
+(** Some big tautologies supplied by John Harrison **)
 
 (*Tautology name: puz013_1.  Auto_tac manages; Blast_tac and Fast_tac take
   a minute or more.*)
diff -r 255055554c67 -r 9ef583b08647 src/HOLCF/IOA/Modelcheck/Cockpit.ML
--- a/src/HOLCF/IOA/Modelcheck/Cockpit.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOLCF/IOA/Modelcheck/Cockpit.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -15,7 +15,7 @@
 qed"cockpit_implements_Info_while_Al";
 
 (* to prove that before any alarm arrives (and after each acknowledgment),
-   info remains at NONE *)
+   info remains at None *)
 Goal "cockpit =<| Info_before_Al";
 by (is_sim_tac aut_simps 1);       
 qed"cockpit_implements_Info_before_Al";
diff -r 255055554c67 -r 9ef583b08647 src/LCF/ex/ROOT.ML
--- a/src/LCF/ex/ROOT.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/LCF/ex/ROOT.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -3,7 +3,7 @@
     Author:     Tobias Nipkow
     Copyright   1991  University of Cambridge
 
-SOME examples from Lawrence Paulson's book Logic and Computation.
+Some examples from Lawrence Paulson's book Logic and Computation.
 *)
 
 time_use_thy "Ex1";
diff -r 255055554c67 -r 9ef583b08647 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/Provers/blast.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -24,7 +24,7 @@
   "Recursive" chains of rules can sometimes exclude other unsafe formulae
 	from expansion.  This happens because newly-created formulae always
 	have priority over existing ones.  But obviously recursive rules 
-	such as transitivity are treated specially to prevent this.  SOMEtimes
+	such as transitivity are treated specially to prevent this.  Sometimes
 	the formulae get into the wrong order (see WRONG below).
 
   With substition for equalities (hyp_subst_tac):
diff -r 255055554c67 -r 9ef583b08647 src/Pure/IsaPlanner/isa_fterm.ML
--- a/src/Pure/IsaPlanner/isa_fterm.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/Pure/IsaPlanner/isa_fterm.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -97,7 +97,7 @@
 open BasicIsaFTerm;
 
 
-(* SOME general search within a focus term... *)
+(* Some general search within a focus term... *)
 
 (* Note: only upterms with a free or constant are going to yeald a
 match, thus if we get anything else (bound or var) skip it! This is