reverted renaming of Some/None in comments and strings;
authorwenzelm
Thu Apr 07 09:25:33 2005 +0200 (2005-04-07)
changeset 156619ef583b08647
parent 15660 255055554c67
child 15662 7e3bee7df06e
reverted renaming of Some/None in comments and strings;
Admin/Benchmarks/HOL-datatype/ROOT.ML
src/CTT/ex/elim.ML
src/Cube/ex/ex.ML
src/FOL/IFOL_lemmas.ML
src/FOL/ex/int.ML
src/FOL/ex/intro.ML
src/FOL/ex/quant.ML
src/FOLP/ex/int.ML
src/FOLP/ex/intro.ML
src/FOLP/ex/quant.ML
src/HOL/Algebra/abstract/order.ML
src/HOL/Hoare/hoare.ML
src/HOL/Hoare/hoareAbort.ML
src/HOL/Import/shuffler.ML
src/HOL/Integ/cooper_dec.ML
src/HOL/Integ/cooper_proof.ML
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/presburger.ML
src/HOL/Real/real_arith.ML
src/HOL/TLA/TLA.ML
src/HOL/Tools/Presburger/cooper_dec.ML
src/HOL/Tools/Presburger/cooper_proof.ML
src/HOL/Tools/Presburger/presburger.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/split_rule.ML
src/HOL/ex/mesontest2.ML
src/HOL/ex/svc_test.ML
src/HOLCF/IOA/Modelcheck/Cockpit.ML
src/LCF/ex/ROOT.ML
src/Provers/blast.ML
src/Pure/IsaPlanner/isa_fterm.ML
     1.1 --- a/Admin/Benchmarks/HOL-datatype/ROOT.ML	Thu Apr 07 09:24:35 2005 +0200
     1.2 +++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML	Thu Apr 07 09:25:33 2005 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Admin/Benchmarks/HOL-datatype/ROOT.ML
     1.5      ID:         $Id$
     1.6  
     1.7 -SOME rather large datatype examples (from John Harrison).
     1.8 +Some rather large datatype examples (from John Harrison).
     1.9  *)
    1.10  
    1.11  val tests = ["Brackin", "Instructions", "SML", "Verilog"];
     2.1 --- a/src/CTT/ex/elim.ML	Thu Apr 07 09:24:35 2005 +0200
     2.2 +++ b/src/CTT/ex/elim.ML	Thu Apr 07 09:25:33 2005 +0200
     2.3 @@ -3,7 +3,7 @@
     2.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.5      Copyright   1991  University of Cambridge
     2.6  
     2.7 -SOME examples taken from P. Martin-L\"of, Intuitionistic type theory
     2.8 +Some examples taken from P. Martin-L\"of, Intuitionistic type theory
     2.9          (Bibliopolis, 1984).
    2.10  
    2.11  by (safe_tac prems 1);
     3.1 --- a/src/Cube/ex/ex.ML	Thu Apr 07 09:24:35 2005 +0200
     3.2 +++ b/src/Cube/ex/ex.ML	Thu Apr 07 09:25:33 2005 +0200
     3.3 @@ -201,7 +201,7 @@
     3.4  by (EVERY[etac pi_elim 1, assume_tac 1, assume_tac 1]);
     3.5  uresult();
     3.6  
     3.7 -(* SOME random examples *)
     3.8 +(* Some random examples *)
     3.9  
    3.10  goal LP2.thy "A:* c:A f:A->A |- \
    3.11  \       Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";
     4.1 --- a/src/FOL/IFOL_lemmas.ML	Thu Apr 07 09:24:35 2005 +0200
     4.2 +++ b/src/FOL/IFOL_lemmas.ML	Thu Apr 07 09:25:33 2005 +0200
     4.3 @@ -204,7 +204,7 @@
     4.4  by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ;
     4.5  qed "ex1I";
     4.6  
     4.7 -(*SOMEtimes easier to use: the premises have no shared variables.  Safe!*)
     4.8 +(*Sometimes easier to use: the premises have no shared variables.  Safe!*)
     4.9  val [ex,eq] = Goal
    4.10      "[| EX x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)";
    4.11  by (rtac (ex RS exE) 1);
     5.1 --- a/src/FOL/ex/int.ML	Thu Apr 07 09:24:35 2005 +0200
     5.2 +++ b/src/FOL/ex/int.ML	Thu Apr 07 09:25:33 2005 +0200
     5.3 @@ -296,7 +296,7 @@
     5.4  writeln"Hard examples with quantifiers";
     5.5  
     5.6  (*The ones that have not been proved are not known to be valid!
     5.7 -  SOME will require quantifier duplication -- not currently available*)
     5.8 +  Some will require quantifier duplication -- not currently available*)
     5.9  
    5.10  writeln"Problem ~~18";
    5.11  Goal "~~(EX y. ALL x. P(y)-->P(x))";
     6.1 --- a/src/FOL/ex/intro.ML	Thu Apr 07 09:24:35 2005 +0200
     6.2 +++ b/src/FOL/ex/intro.ML	Thu Apr 07 09:25:33 2005 +0200
     6.3 @@ -14,7 +14,7 @@
     6.4  
     6.5  context FOL.thy;
     6.6  
     6.7 -(**** SOME simple backward proofs ****)
     6.8 +(**** Some simple backward proofs ****)
     6.9  
    6.10  Goal "P|P --> P";
    6.11  by (rtac impI 1);
     7.1 --- a/src/FOL/ex/quant.ML	Thu Apr 07 09:24:35 2005 +0200
     7.2 +++ b/src/FOL/ex/quant.ML	Thu Apr 07 09:25:33 2005 +0200
     7.3 @@ -34,7 +34,7 @@
     7.4  result();  
     7.5  
     7.6  
     7.7 -writeln"SOME harder ones";
     7.8 +writeln"Some harder ones";
     7.9  
    7.10  Goal "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
    7.11  by tac;
    7.12 @@ -104,7 +104,7 @@
    7.13  result();  
    7.14  
    7.15  
    7.16 -writeln"SOME slow ones";
    7.17 +writeln"Some slow ones";
    7.18  
    7.19  
    7.20  (*Principia Mathematica *11.53  *)
     8.1 --- a/src/FOLP/ex/int.ML	Thu Apr 07 09:24:35 2005 +0200
     8.2 +++ b/src/FOLP/ex/int.ML	Thu Apr 07 09:25:33 2005 +0200
     8.3 @@ -231,7 +231,7 @@
     8.4  writeln"Hard examples with quantifiers";
     8.5  
     8.6  (*The ones that have not been proved are not known to be valid!
     8.7 -  SOME will require quantifier duplication -- not currently available*)
     8.8 +  Some will require quantifier duplication -- not currently available*)
     8.9  
    8.10  writeln"Problem ~~18";
    8.11  goal IFOLP.thy "?p : ~~(EX y. ALL x. P(y)-->P(x))";
     9.1 --- a/src/FOLP/ex/intro.ML	Thu Apr 07 09:24:35 2005 +0200
     9.2 +++ b/src/FOLP/ex/intro.ML	Thu Apr 07 09:25:33 2005 +0200
     9.3 @@ -12,7 +12,7 @@
     9.4  *)
     9.5  
     9.6  
     9.7 -(**** SOME simple backward proofs ****)
     9.8 +(**** Some simple backward proofs ****)
     9.9  
    9.10  goal FOLP.thy "?p:P|P --> P";
    9.11  by (rtac impI 1);
    10.1 --- a/src/FOLP/ex/quant.ML	Thu Apr 07 09:24:35 2005 +0200
    10.2 +++ b/src/FOLP/ex/quant.ML	Thu Apr 07 09:25:33 2005 +0200
    10.3 @@ -34,7 +34,7 @@
    10.4  result();  
    10.5  
    10.6  
    10.7 -writeln"SOME harder ones";
    10.8 +writeln"Some harder ones";
    10.9  
   10.10  Goal "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
   10.11  by tac;
   10.12 @@ -104,7 +104,7 @@
   10.13  result();  
   10.14  
   10.15  
   10.16 -writeln"SOME slow ones";
   10.17 +writeln"Some slow ones";
   10.18  
   10.19  
   10.20  (*Principia Mathematica *11.53  *)
    11.1 --- a/src/HOL/Algebra/abstract/order.ML	Thu Apr 07 09:24:35 2005 +0200
    11.2 +++ b/src/HOL/Algebra/abstract/order.ML	Thu Apr 07 09:25:33 2005 +0200
    11.3 @@ -60,7 +60,7 @@
    11.4  
    11.5  fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);
    11.6  
    11.7 -(* SOME code useful for debugging
    11.8 +(* Some code useful for debugging
    11.9  
   11.10  val intT = HOLogic.intT;
   11.11  val a = Free ("a", intT);
    12.1 --- a/src/HOL/Hoare/hoare.ML	Thu Apr 07 09:24:35 2005 +0200
    12.2 +++ b/src/HOL/Hoare/hoare.ML	Thu Apr 07 09:25:33 2005 +0200
    12.3 @@ -89,7 +89,7 @@
    12.4  
    12.5  (*****************************************************************************)
    12.6  (** Simplifying:                                                            **)
    12.7 -(** SOME useful lemmata, lists and simplification tactics to control which  **)
    12.8 +(** Some useful lemmata, lists and simplification tactics to control which  **)
    12.9  (** theorems are used to simplify at each moment, so that the original      **)
   12.10  (** input does not suffer any unexpected transformation                     **)
   12.11  (*****************************************************************************)
    13.1 --- a/src/HOL/Hoare/hoareAbort.ML	Thu Apr 07 09:24:35 2005 +0200
    13.2 +++ b/src/HOL/Hoare/hoareAbort.ML	Thu Apr 07 09:25:33 2005 +0200
    13.3 @@ -90,7 +90,7 @@
    13.4  
    13.5  (*****************************************************************************)
    13.6  (** Simplifying:                                                            **)
    13.7 -(** SOME useful lemmata, lists and simplification tactics to control which  **)
    13.8 +(** Some useful lemmata, lists and simplification tactics to control which  **)
    13.9  (** theorems are used to simplify at each moment, so that the original      **)
   13.10  (** input does not suffer any unexpected transformation                     **)
   13.11  (*****************************************************************************)
    14.1 --- a/src/HOL/Import/shuffler.ML	Thu Apr 07 09:24:35 2005 +0200
    14.2 +++ b/src/HOL/Import/shuffler.ML	Thu Apr 07 09:25:33 2005 +0200
    14.3 @@ -304,7 +304,7 @@
    14.4  		val lhs = #1 (Logic.dest_equals (prop_of (final init)))
    14.5  	    in
    14.6  		if not (lhs aconv origt)
    14.7 -		then (writeln "SOMEthing is utterly wrong: (orig,lhs,frozen type,t,tinst)";
    14.8 +		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
    14.9  		      writeln (string_of_cterm (cterm_of sg origt));
   14.10  		      writeln (string_of_cterm (cterm_of sg lhs));
   14.11  		      writeln (string_of_cterm (cterm_of sg typet));
   14.12 @@ -359,7 +359,7 @@
   14.13  		val lhs = #1 (Logic.dest_equals (prop_of (final init)))
   14.14  	    in
   14.15  		if not (lhs aconv origt)
   14.16 -		then (writeln "SOMEthing is utterly wrong: (orig,lhs,frozen type,t,tinst)";
   14.17 +		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
   14.18  		      writeln (string_of_cterm (cterm_of sg origt));
   14.19  		      writeln (string_of_cterm (cterm_of sg lhs));
   14.20  		      writeln (string_of_cterm (cterm_of sg typet));
    15.1 --- a/src/HOL/Integ/cooper_dec.ML	Thu Apr 07 09:24:35 2005 +0200
    15.2 +++ b/src/HOL/Integ/cooper_dec.ML	Thu Apr 07 09:25:33 2005 +0200
    15.3 @@ -92,7 +92,7 @@
    15.4  fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
    15.5     |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
    15.6     |dest_numeral (Const ("Numeral.number_of",_) $ n)= HOLogic.dest_binum n; 
    15.7 -(*SOME terms often used for pattern matching*) 
    15.8 +(*Some terms often used for pattern matching*) 
    15.9   
   15.10  val zero = mk_numeral 0; 
   15.11  val one = mk_numeral 1; 
    16.1 --- a/src/HOL/Integ/cooper_proof.ML	Thu Apr 07 09:24:35 2005 +0200
    16.2 +++ b/src/HOL/Integ/cooper_proof.ML	Thu Apr 07 09:25:33 2005 +0200
    16.3 @@ -380,7 +380,7 @@
    16.4  (*==================================================*)
    16.5  fun rho_for_modd_minf x dlcm sg fm1 =
    16.6  let
    16.7 -    (*SOME certified Terms*)
    16.8 +    (*Some certified Terms*)
    16.9      
   16.10     val ctrue = cterm_of sg HOLogic.true_const
   16.11     val cfalse = cterm_of sg HOLogic.false_const
   16.12 @@ -476,7 +476,7 @@
   16.13  (* -------------------------------------------------------------*)
   16.14  fun rho_for_modd_pinf x dlcm sg fm1 = 
   16.15  let
   16.16 -    (*SOME certified Terms*)
   16.17 +    (*Some certified Terms*)
   16.18      
   16.19    val ctrue = cterm_of sg HOLogic.true_const
   16.20    val cfalse = cterm_of sg HOLogic.false_const
    17.1 --- a/src/HOL/Integ/int_arith1.ML	Thu Apr 07 09:24:35 2005 +0200
    17.2 +++ b/src/HOL/Integ/int_arith1.ML	Thu Apr 07 09:25:33 2005 +0200
    17.3 @@ -538,7 +538,7 @@
    17.4  Addsimprocs [fast_int_arith_simproc]
    17.5  
    17.6  
    17.7 -(* SOME test data
    17.8 +(* Some test data
    17.9  Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
   17.10  by (fast_arith_tac 1);
   17.11  Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)";
    18.1 --- a/src/HOL/Integ/presburger.ML	Thu Apr 07 09:24:35 2005 +0200
    18.2 +++ b/src/HOL/Integ/presburger.ML	Thu Apr 07 09:25:33 2005 +0200
    18.3 @@ -73,7 +73,7 @@
    18.4  
    18.5  fun term_typed_consts t = add_term_typed_consts(t,[]);
    18.6  
    18.7 -(* SOME Types*)
    18.8 +(* Some Types*)
    18.9  val bT = HOLogic.boolT;
   18.10  val bitT = HOLogic.bitT;
   18.11  val iT = HOLogic.intT;
   18.12 @@ -249,7 +249,7 @@
   18.13      val g' = if a then abstract_pres sg g else g
   18.14      (* Transform the term*)
   18.15      val (t,np,nh) = prepare_for_presburger sg q g'
   18.16 -    (* SOME simpsets for dealing with mod div abs and nat*)
   18.17 +    (* Some simpsets for dealing with mod div abs and nat*)
   18.18      val simpset0 = HOL_basic_ss
   18.19        addsimps [mod_div_equality', Suc_plus1]
   18.20        addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
    19.1 --- a/src/HOL/Real/real_arith.ML	Thu Apr 07 09:24:35 2005 +0200
    19.2 +++ b/src/HOL/Real/real_arith.ML	Thu Apr 07 09:25:33 2005 +0200
    19.3 @@ -136,7 +136,7 @@
    19.4  end;
    19.5  
    19.6  
    19.7 -(* SOME test data [omitting examples that assume the ordering to be discrete!]
    19.8 +(* Some test data [omitting examples that assume the ordering to be discrete!]
    19.9  Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
   19.10  by (fast_arith_tac 1);
   19.11  qed "";
    20.1 --- a/src/HOL/TLA/TLA.ML	Thu Apr 07 09:24:35 2005 +0200
    20.2 +++ b/src/HOL/TLA/TLA.ML	Thu Apr 07 09:25:33 2005 +0200
    20.3 @@ -818,7 +818,7 @@
    20.4  by (asm_simp_tac (simpset() addsimps [split_box_conj,box_stp_actI]) 1);
    20.5  qed "WF1";
    20.6  
    20.7 -(* SOMEtimes easier to use; designed for action B rather than state predicate Q *)
    20.8 +(* Sometimes easier to use; designed for action B rather than state predicate Q *)
    20.9  val [prem1,prem2,prem3] = goalw thy [leadsto_def]
   20.10    "[| |- N & $P --> $Enabled (<A>_v);            \
   20.11  \     |- N & <A>_v --> B;                  \ 
    21.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Thu Apr 07 09:24:35 2005 +0200
    21.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Thu Apr 07 09:25:33 2005 +0200
    21.3 @@ -92,7 +92,7 @@
    21.4  fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
    21.5     |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
    21.6     |dest_numeral (Const ("Numeral.number_of",_) $ n)= HOLogic.dest_binum n; 
    21.7 -(*SOME terms often used for pattern matching*) 
    21.8 +(*Some terms often used for pattern matching*) 
    21.9   
   21.10  val zero = mk_numeral 0; 
   21.11  val one = mk_numeral 1; 
    22.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML	Thu Apr 07 09:24:35 2005 +0200
    22.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Thu Apr 07 09:25:33 2005 +0200
    22.3 @@ -380,7 +380,7 @@
    22.4  (*==================================================*)
    22.5  fun rho_for_modd_minf x dlcm sg fm1 =
    22.6  let
    22.7 -    (*SOME certified Terms*)
    22.8 +    (*Some certified Terms*)
    22.9      
   22.10     val ctrue = cterm_of sg HOLogic.true_const
   22.11     val cfalse = cterm_of sg HOLogic.false_const
   22.12 @@ -476,7 +476,7 @@
   22.13  (* -------------------------------------------------------------*)
   22.14  fun rho_for_modd_pinf x dlcm sg fm1 = 
   22.15  let
   22.16 -    (*SOME certified Terms*)
   22.17 +    (*Some certified Terms*)
   22.18      
   22.19    val ctrue = cterm_of sg HOLogic.true_const
   22.20    val cfalse = cterm_of sg HOLogic.false_const
    23.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Thu Apr 07 09:24:35 2005 +0200
    23.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Thu Apr 07 09:25:33 2005 +0200
    23.3 @@ -73,7 +73,7 @@
    23.4  
    23.5  fun term_typed_consts t = add_term_typed_consts(t,[]);
    23.6  
    23.7 -(* SOME Types*)
    23.8 +(* Some Types*)
    23.9  val bT = HOLogic.boolT;
   23.10  val bitT = HOLogic.bitT;
   23.11  val iT = HOLogic.intT;
   23.12 @@ -249,7 +249,7 @@
   23.13      val g' = if a then abstract_pres sg g else g
   23.14      (* Transform the term*)
   23.15      val (t,np,nh) = prepare_for_presburger sg q g'
   23.16 -    (* SOME simpsets for dealing with mod div abs and nat*)
   23.17 +    (* Some simpsets for dealing with mod div abs and nat*)
   23.18      val simpset0 = HOL_basic_ss
   23.19        addsimps [mod_div_equality', Suc_plus1]
   23.20        addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
    24.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Apr 07 09:24:35 2005 +0200
    24.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Apr 07 09:25:33 2005 +0200
    24.3 @@ -945,7 +945,7 @@
    24.4      val dt_info = get_datatypes thy;
    24.5      val (descr, _) = unfold_datatypes sign dts' sorts dt_info dts' i;
    24.6      val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
    24.7 -      if err then error ("NONEmptiness check failed for datatype " ^ s)
    24.8 +      if err then error ("Nonemptiness check failed for datatype " ^ s)
    24.9        else raise exn;
   24.10  
   24.11      val descr' = List.concat descr;
    25.1 --- a/src/HOL/Tools/split_rule.ML	Thu Apr 07 09:24:35 2005 +0200
    25.2 +++ b/src/HOL/Tools/split_rule.ML	Thu Apr 07 09:25:33 2005 +0200
    25.3 @@ -2,7 +2,7 @@
    25.4      ID:         $Id$
    25.5      Author:     Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen
    25.6  
    25.7 -SOME tools for managing tupled arguments and abstractions in rules.
    25.8 +Some tools for managing tupled arguments and abstractions in rules.
    25.9  *)
   25.10  
   25.11  signature BASIC_SPLIT_RULE =
   25.12 @@ -130,6 +130,8 @@
   25.13  
   25.14  (* attribute syntax *)
   25.15  
   25.16 +(* FIXME dynamically scoped due to Args.name/pair_tac *)
   25.17 +
   25.18  fun split_format x = Attrib.syntax
   25.19    (Scan.lift (Args.parens (Args.$$$ "complete"))
   25.20      >> K (Drule.rule_attribute (K complete_split_rule)) ||
    26.1 --- a/src/HOL/ex/mesontest2.ML	Thu Apr 07 09:24:35 2005 +0200
    26.2 +++ b/src/HOL/ex/mesontest2.ML	Thu Apr 07 09:25:33 2005 +0200
    26.3 @@ -193,7 +193,7 @@
    26.4  (*
    26.5   * Original timings for John Harrison's MESON_TAC.
    26.6   * Timings below on a 600MHz Pentium III (perch)
    26.7 - * SOME timings below refer to griffon, which is a dual 2.5GHz Power Mac G5.
    26.8 + * Some timings below refer to griffon, which is a dual 2.5GHz Power Mac G5.
    26.9   * 
   26.10   * A few variable names have been changed to avoid clashing with constants.
   26.11   *
    27.1 --- a/src/HOL/ex/svc_test.ML	Thu Apr 07 09:24:35 2005 +0200
    27.2 +++ b/src/HOL/ex/svc_test.ML	Thu Apr 07 09:25:33 2005 +0200
    27.3 @@ -18,7 +18,7 @@
    27.4  by (svc_tac 1);
    27.5  qed "";
    27.6  
    27.7 -(** SOME big tautologies supplied by John Harrison **)
    27.8 +(** Some big tautologies supplied by John Harrison **)
    27.9  
   27.10  (*Tautology name: puz013_1.  Auto_tac manages; Blast_tac and Fast_tac take
   27.11    a minute or more.*)
    28.1 --- a/src/HOLCF/IOA/Modelcheck/Cockpit.ML	Thu Apr 07 09:24:35 2005 +0200
    28.2 +++ b/src/HOLCF/IOA/Modelcheck/Cockpit.ML	Thu Apr 07 09:25:33 2005 +0200
    28.3 @@ -15,7 +15,7 @@
    28.4  qed"cockpit_implements_Info_while_Al";
    28.5  
    28.6  (* to prove that before any alarm arrives (and after each acknowledgment),
    28.7 -   info remains at NONE *)
    28.8 +   info remains at None *)
    28.9  Goal "cockpit =<| Info_before_Al";
   28.10  by (is_sim_tac aut_simps 1);       
   28.11  qed"cockpit_implements_Info_before_Al";
    29.1 --- a/src/LCF/ex/ROOT.ML	Thu Apr 07 09:24:35 2005 +0200
    29.2 +++ b/src/LCF/ex/ROOT.ML	Thu Apr 07 09:25:33 2005 +0200
    29.3 @@ -3,7 +3,7 @@
    29.4      Author:     Tobias Nipkow
    29.5      Copyright   1991  University of Cambridge
    29.6  
    29.7 -SOME examples from Lawrence Paulson's book Logic and Computation.
    29.8 +Some examples from Lawrence Paulson's book Logic and Computation.
    29.9  *)
   29.10  
   29.11  time_use_thy "Ex1";
    30.1 --- a/src/Provers/blast.ML	Thu Apr 07 09:24:35 2005 +0200
    30.2 +++ b/src/Provers/blast.ML	Thu Apr 07 09:25:33 2005 +0200
    30.3 @@ -24,7 +24,7 @@
    30.4    "Recursive" chains of rules can sometimes exclude other unsafe formulae
    30.5  	from expansion.  This happens because newly-created formulae always
    30.6  	have priority over existing ones.  But obviously recursive rules 
    30.7 -	such as transitivity are treated specially to prevent this.  SOMEtimes
    30.8 +	such as transitivity are treated specially to prevent this.  Sometimes
    30.9  	the formulae get into the wrong order (see WRONG below).
   30.10  
   30.11    With substition for equalities (hyp_subst_tac):
    31.1 --- a/src/Pure/IsaPlanner/isa_fterm.ML	Thu Apr 07 09:24:35 2005 +0200
    31.2 +++ b/src/Pure/IsaPlanner/isa_fterm.ML	Thu Apr 07 09:25:33 2005 +0200
    31.3 @@ -97,7 +97,7 @@
    31.4  open BasicIsaFTerm;
    31.5  
    31.6  
    31.7 -(* SOME general search within a focus term... *)
    31.8 +(* Some general search within a focus term... *)
    31.9  
   31.10  (* Note: only upterms with a free or constant are going to yeald a
   31.11  match, thus if we get anything else (bound or var) skip it! This is