--- 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"];
--- 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);
--- 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";
--- 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);
--- 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))";
--- 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);
--- 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 *)
--- 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))";
--- 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);
--- 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 *)
--- 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);
--- 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 **)
(*****************************************************************************)
--- 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 **)
(*****************************************************************************)
--- 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));
--- 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;
--- 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
--- 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)";
--- 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]
--- 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 "";
--- 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; \
--- 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;
--- 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
--- 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]
--- 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;
--- 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)) ||
--- 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.
*
--- 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.*)
--- 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";
--- 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";
--- 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):
--- 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