eliminated hard tabs;
authorwenzelm
Sat Aug 29 12:01:25 2009 +0200 (2009-08-29)
changeset 32449696d64ed85da
parent 32448 a89f876731c5
child 32450 375db037f4d2
eliminated hard tabs;
Admin/isatest/annomaly.ML
doc-src/rail.ML
src/FOL/fologic.ML
src/FOL/intprover.ML
src/FOLP/hypsubst.ML
src/FOLP/simp.ML
src/HOL/Algebra/abstract/Ring2.thy
     1.1 --- a/Admin/isatest/annomaly.ML	Sat Aug 29 10:50:04 2009 +0200
     1.2 +++ b/Admin/isatest/annomaly.ML	Sat Aug 29 12:01:25 2009 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4    val isabelleHome =
     1.5        case OS.Process.getEnv "ISABELLE_HOME"
     1.6         of  NONE => OS.FileSys.getDir ()
     1.7 -	 | SOME home => mkAbsolute home
     1.8 +         | SOME home => mkAbsolute home
     1.9  
    1.10    fun noparent [] = []
    1.11      | noparent (n :: ns) =
    1.12 @@ -33,12 +33,12 @@
    1.13  
    1.14    fun rewrite defPrefix name =
    1.15        let val abs = mkAbsolute name
    1.16 -	  val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome }
    1.17 -	  val exists = (OS.FileSys.access(abs, nil)
    1.18 -			handle OS.SysErr _ => false)
    1.19 +          val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome }
    1.20 +          val exists = (OS.FileSys.access(abs, nil)
    1.21 +                        handle OS.SysErr _ => false)
    1.22        in  if exists andalso rel <> ""
    1.23 -	  then isabellePath (toArcs rel)
    1.24 -	  else defPrefix @ noparent (toArcs name)
    1.25 +          then isabellePath (toArcs rel)
    1.26 +          else defPrefix @ noparent (toArcs name)
    1.27        end handle OS.Path.Path => defPrefix @ noparent (toArcs name)
    1.28  
    1.29  in
    1.30 @@ -49,10 +49,10 @@
    1.31          (* should we have different files for different line numbers? *
    1.32          val arcs = if line <= 1 then arcs
    1.33                     else arcs @ [ "l." ^ Int.toString line ]
    1.34 -	*)
    1.35 -	val arcs = if t = "structure Isabelle =\nstruct\nend;"
    1.36 -		      andalso name = "ML"
    1.37 -		   then ["empty_Isabelle", "empty" ] else arcs
    1.38 +        *)
    1.39 +        val arcs = if t = "structure Isabelle =\nstruct\nend;"
    1.40 +                      andalso name = "ML"
    1.41 +                   then ["empty_Isabelle", "empty" ] else arcs
    1.42          val _    = AnnoMaLy.nameNextStream arcs
    1.43      in  smlnj_use_text tune str_of_pos name_space (line, name) p v t  end;
    1.44  
     2.1 --- a/doc-src/rail.ML	Sat Aug 29 10:50:04 2009 +0200
     2.2 +++ b/doc-src/rail.ML	Sat Aug 29 12:01:25 2009 +0200
     2.3 @@ -99,7 +99,7 @@
     2.4        |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
     2.5        |> (if ! ThyOutput.quotes then quote else I)
     2.6        |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
     2.7 -	  else hyper o enclose "\\mbox{\\isa{" "}}")), style)
     2.8 +          else hyper o enclose "\\mbox{\\isa{" "}}")), style)
     2.9    else ("Bad " ^ kind ^ " " ^ name, false)
    2.10    end;
    2.11  end;
    2.12 @@ -147,8 +147,8 @@
    2.13    ) >> (Identifier o enclose "\\isa{" "}" o Output.output o implode) ||
    2.14    scan_link >> (decode_link ctxt) >>
    2.15      (fn (txt, style) =>
    2.16 -	if style then Special_Identifier(txt)
    2.17 -	else Identifier(txt))
    2.18 +        if style then Special_Identifier(txt)
    2.19 +        else Identifier(txt))
    2.20  end;
    2.21  
    2.22  fun scan_anot ctxt =
    2.23 @@ -169,12 +169,12 @@
    2.24      val text_sq =
    2.25        Scan.repeat (
    2.26          Scan.one (fn s =>
    2.27 -	  s <> "\n" andalso
    2.28 -	  s <> "\t" andalso
    2.29 -	  s <> "'" andalso
    2.30 -	  s <> "\\" andalso
    2.31 -	  Symbol.is_regular s) ||
    2.32 -	($$ "\\" |-- $$ "'")
    2.33 +          s <> "\n" andalso
    2.34 +          s <> "\t" andalso
    2.35 +          s <> "'" andalso
    2.36 +          s <> "\\" andalso
    2.37 +          Symbol.is_regular s) ||
    2.38 +        ($$ "\\" |-- $$ "'")
    2.39        ) >> implode
    2.40    fun quoted scan = $$ "'" |-- scan --| $$ "'";
    2.41    in
    2.42 @@ -305,9 +305,9 @@
    2.43    parse_body2 -- ($$$ "*" |-- !!! "body4e expected" (parse_body4e)) >>
    2.44      (fn (body1, body2) =>
    2.45        if is_empty body2 then
    2.46 -	add_body(PLUS, new_empty_body, rev_body body1)
    2.47 +        add_body(PLUS, new_empty_body, rev_body body1)
    2.48        else
    2.49 -	add_body(BAR, new_empty_body, add_body (PLUS, body1, rev_body body2)) ) ||
    2.50 +        add_body(BAR, new_empty_body, add_body (PLUS, body1, rev_body body2)) ) ||
    2.51    parse_body2 -- ($$$ "+" |-- !!! "body4e expected" (parse_body4e)) >>
    2.52      (fn (body1, body2) => new_body (PLUS, body1, rev_body body2) ) ||
    2.53    parse_body2e
    2.54 @@ -365,36 +365,36 @@
    2.55  fun position_body (body as Body(kind, text, annot, id, bodies), ystart) =
    2.56    let fun max (x,y) = if x > y then x else y
    2.57      fun set_body_position (Body(kind, text, annot, id, bodies), ystart, ynext) =
    2.58 -	  Body_Pos(kind, text, annot, id, bodies, ystart, ynext)
    2.59 +          Body_Pos(kind, text, annot, id, bodies, ystart, ynext)
    2.60      fun pos_bodies_cat ([],_,ynext,liste) = (liste, ynext)
    2.61        | pos_bodies_cat (x::xs, ystart, ynext, liste) =
    2.62 -	  if is_kind_of CR x then
    2.63 -	      (case set_body_position(x, ystart, ynext+1) of
    2.64 -		body as Body_Pos(_,_,_,_,_,_,ynext1) =>
    2.65 -		  pos_bodies_cat(xs, ynext1, max(ynext,ynext1), liste@[body])
    2.66 -	      )
    2.67 -	  else
    2.68 -	      (case position_body(x, ystart) of
    2.69 -		body as Body_Pos(_,_,_,_,_,_,ynext1) =>
    2.70 -		  pos_bodies_cat(xs, ystart, max(ynext,ynext1), liste@[body])
    2.71 -	      )
    2.72 +          if is_kind_of CR x then
    2.73 +              (case set_body_position(x, ystart, ynext+1) of
    2.74 +                body as Body_Pos(_,_,_,_,_,_,ynext1) =>
    2.75 +                  pos_bodies_cat(xs, ynext1, max(ynext,ynext1), liste@[body])
    2.76 +              )
    2.77 +          else
    2.78 +              (case position_body(x, ystart) of
    2.79 +                body as Body_Pos(_,_,_,_,_,_,ynext1) =>
    2.80 +                  pos_bodies_cat(xs, ystart, max(ynext,ynext1), liste@[body])
    2.81 +              )
    2.82      fun pos_bodies_bar_plus ([],_,ynext,liste) = (liste, ynext)
    2.83        | pos_bodies_bar_plus (x::xs, ystart, ynext, liste) =
    2.84 -	  (case position_body(x, ystart) of
    2.85 -	    body as Body_Pos(_,_,_,_,_,_,ynext1) =>
    2.86 -	      pos_bodies_bar_plus(xs, ynext1, max(ynext,ynext1), liste@[body])
    2.87 -	  )
    2.88 +          (case position_body(x, ystart) of
    2.89 +            body as Body_Pos(_,_,_,_,_,_,ynext1) =>
    2.90 +              pos_bodies_bar_plus(xs, ynext1, max(ynext,ynext1), liste@[body])
    2.91 +          )
    2.92    in
    2.93    (case kind of
    2.94      CAT => (case pos_bodies_cat(bodies,ystart,ystart+1,[]) of
    2.95 -	      (bodiesPos, ynext) =>
    2.96 -		Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
    2.97 +              (bodiesPos, ynext) =>
    2.98 +                Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
    2.99    | BAR => (case pos_bodies_bar_plus(bodies,ystart,ystart+1,[]) of
   2.100 -	      (bodiesPos, ynext) =>
   2.101 -		Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
   2.102 +              (bodiesPos, ynext) =>
   2.103 +                Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
   2.104    | PLUS => (case pos_bodies_bar_plus(bodies,ystart,ystart+1,[]) of
   2.105 -	      (bodiesPos, ynext) =>
   2.106 -		Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
   2.107 +              (bodiesPos, ynext) =>
   2.108 +                Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
   2.109    | CR => set_body_position(body, ystart, ystart+3)
   2.110    | EMPTY => set_body_position(body, ystart, ystart+1)
   2.111    | ANNOTE => set_body_position(body, ystart, ystart+1)
   2.112 @@ -406,15 +406,15 @@
   2.113  fun format_body (Body_Pos(EMPTY,_,_,_,_,_,_), _) = ""
   2.114    | format_body (Body_Pos(CAT,_,_,_,bodies,_,_), cent) =
   2.115      let fun format_bodies([]) = ""
   2.116 -	  | format_bodies(x::xs) = format_body (x, "") ^ format_bodies(xs)
   2.117 +          | format_bodies(x::xs) = format_body (x, "") ^ format_bodies(xs)
   2.118      in
   2.119        format_bodies(bodies)
   2.120      end
   2.121    | format_body (Body_Pos(BAR,_,_,_,bodies,_,_),cent) =
   2.122      let fun format_bodies([]) = "\\rail@endbar\n"
   2.123 -	  | format_bodies(x::xs) =
   2.124 -	      "\\rail@nextbar{" ^ string_of_int(getystart(x)) ^"}\n" ^
   2.125 -	      format_body(x, "") ^ format_bodies(xs)
   2.126 +          | format_bodies(x::xs) =
   2.127 +              "\\rail@nextbar{" ^ string_of_int(getystart(x)) ^"}\n" ^
   2.128 +              format_body(x, "") ^ format_bodies(xs)
   2.129      in
   2.130        "\\rail@bar\n" ^ format_body(hd(bodies), "") ^ format_bodies(tl(bodies))
   2.131      end
     3.1 --- a/src/FOL/fologic.ML	Sat Aug 29 10:50:04 2009 +0200
     3.2 +++ b/src/FOL/fologic.ML	Sat Aug 29 12:01:25 2009 +0200
     3.3 @@ -6,28 +6,28 @@
     3.4  
     3.5  signature FOLOGIC =
     3.6  sig
     3.7 -  val oT		: typ
     3.8 -  val mk_Trueprop	: term -> term
     3.9 -  val dest_Trueprop	: term -> term
    3.10 -  val not		: term
    3.11 -  val conj		: term
    3.12 -  val disj		: term
    3.13 -  val imp		: term
    3.14 -  val iff		: term
    3.15 -  val mk_conj		: term * term -> term
    3.16 -  val mk_disj		: term * term -> term
    3.17 -  val mk_imp		: term * term -> term
    3.18 -  val dest_imp	       	: term -> term*term
    3.19 -  val dest_conj         : term -> term list
    3.20 -  val mk_iff		: term * term -> term
    3.21 -  val dest_iff	       	: term -> term*term
    3.22 -  val all_const		: typ -> term
    3.23 -  val mk_all		: term * term -> term
    3.24 -  val exists_const	: typ -> term
    3.25 -  val mk_exists		: term * term -> term
    3.26 -  val eq_const		: typ -> term
    3.27 -  val mk_eq		: term * term -> term
    3.28 -  val dest_eq 		: term -> term*term
    3.29 +  val oT: typ
    3.30 +  val mk_Trueprop: term -> term
    3.31 +  val dest_Trueprop: term -> term
    3.32 +  val not: term
    3.33 +  val conj: term
    3.34 +  val disj: term
    3.35 +  val imp: term
    3.36 +  val iff: term
    3.37 +  val mk_conj: term * term -> term
    3.38 +  val mk_disj: term * term -> term
    3.39 +  val mk_imp: term * term -> term
    3.40 +  val dest_imp: term -> term * term
    3.41 +  val dest_conj: term -> term list
    3.42 +  val mk_iff: term * term -> term
    3.43 +  val dest_iff: term -> term * term
    3.44 +  val all_const: typ -> term
    3.45 +  val mk_all: term * term -> term
    3.46 +  val exists_const: typ -> term
    3.47 +  val mk_exists: term * term -> term
    3.48 +  val eq_const: typ -> term
    3.49 +  val mk_eq: term * term -> term
    3.50 +  val dest_eq: term -> term * term
    3.51    val mk_binop: string -> term * term -> term
    3.52    val mk_binrel: string -> term * term -> term
    3.53    val dest_bin: string -> typ -> term -> term * term
    3.54 @@ -46,7 +46,8 @@
    3.55  fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
    3.56    | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
    3.57  
    3.58 -(** Logical constants **)
    3.59 +
    3.60 +(* Logical constants *)
    3.61  
    3.62  val not = Const ("Not", oT --> oT);
    3.63  val conj = Const("op &", [oT,oT]--->oT);
    3.64 @@ -80,6 +81,7 @@
    3.65  fun exists_const T = Const ("Ex", [T --> oT] ---> oT);
    3.66  fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
    3.67  
    3.68 +
    3.69  (* binary oprations and relations *)
    3.70  
    3.71  fun mk_binop c (t, u) =
    3.72 @@ -97,5 +99,4 @@
    3.73        else raise TERM ("dest_bin " ^ c, [tm])
    3.74    | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
    3.75  
    3.76 -
    3.77  end;
     4.1 --- a/src/FOL/intprover.ML	Sat Aug 29 10:50:04 2009 +0200
     4.2 +++ b/src/FOL/intprover.ML	Sat Aug 29 12:01:25 2009 +0200
     4.3 @@ -79,8 +79,7 @@
     4.4  (*One safe or unsafe step. *)
     4.5  fun step_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_brls i];
     4.6  
     4.7 -fun step_dup_tac i = FIRST [safe_tac, inst_step_tac i, 
     4.8 -			    biresolve_tac haz_dup_brls i];
     4.9 +fun step_dup_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_dup_brls i];
    4.10  
    4.11  (*Dumb but fast*)
    4.12  val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1));
     5.1 --- a/src/FOLP/hypsubst.ML	Sat Aug 29 10:50:04 2009 +0200
     5.2 +++ b/src/FOLP/hypsubst.ML	Sat Aug 29 12:01:25 2009 +0200
     5.3 @@ -27,7 +27,7 @@
     5.4    val inspect_pair        : bool -> term * term -> thm
     5.5    end;
     5.6  
     5.7 -functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
     5.8 +functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
     5.9  struct
    5.10  
    5.11  local open Data in
    5.12 @@ -43,13 +43,13 @@
    5.13      but how could we check for this?*)
    5.14  fun inspect_pair bnd (t,u) =
    5.15    case (Envir.eta_contract t, Envir.eta_contract u) of
    5.16 -       (Bound i, _) => if loose(i,u) then raise Match 
    5.17 +       (Bound i, _) => if loose(i,u) then raise Match
    5.18                         else sym         (*eliminates t*)
    5.19 -     | (_, Bound i) => if loose(i,t) then raise Match 
    5.20 +     | (_, Bound i) => if loose(i,t) then raise Match
    5.21                         else asm_rl      (*eliminates u*)
    5.22 -     | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match 
    5.23 +     | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match
    5.24                        else sym          (*eliminates t*)
    5.25 -     | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match 
    5.26 +     | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match
    5.27                        else asm_rl       (*eliminates u*)
    5.28       | _ => raise Match;
    5.29  
    5.30 @@ -58,7 +58,7 @@
    5.31     the rule asm_rl (resp. sym). *)
    5.32  fun eq_var bnd =
    5.33    let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
    5.34 -        | eq_var_aux k (Const("==>",_) $ A $ B) = 
    5.35 +        | eq_var_aux k (Const("==>",_) $ A $ B) =
    5.36                ((k, inspect_pair bnd (dest_eq A))
    5.37                        (*Exception Match comes from inspect_pair or dest_eq*)
    5.38                 handle Match => eq_var_aux (k+1) B)
    5.39 @@ -70,13 +70,13 @@
    5.40  fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
    5.41        let val n = length(Logic.strip_assums_hyp Bi) - 1
    5.42            val (k,symopt) = eq_var bnd Bi
    5.43 -      in 
    5.44 +      in
    5.45           DETERM
    5.46             (EVERY [REPEAT_DETERM_N k (etac rev_mp i),
    5.47 -		   etac revcut_rl i,
    5.48 -		   REPEAT_DETERM_N (n-k) (etac rev_mp i),
    5.49 -		   etac (symopt RS subst) i,
    5.50 -		   REPEAT_DETERM_N n (rtac imp_intr i)])
    5.51 +                   etac revcut_rl i,
    5.52 +                   REPEAT_DETERM_N (n-k) (etac rev_mp i),
    5.53 +                   etac (symopt RS subst) i,
    5.54 +                   REPEAT_DETERM_N n (rtac imp_intr i)])
    5.55        end
    5.56        handle THM _ => no_tac | EQ_VAR => no_tac);
    5.57  
     6.1 --- a/src/FOLP/simp.ML	Sat Aug 29 10:50:04 2009 +0200
     6.2 +++ b/src/FOLP/simp.ML	Sat Aug 29 12:01:25 2009 +0200
     6.3 @@ -52,7 +52,7 @@
     6.4    val tracing   : bool ref
     6.5  end;
     6.6  
     6.7 -functor SimpFun (Simp_data: SIMP_DATA) : SIMP = 
     6.8 +functor SimpFun (Simp_data: SIMP_DATA) : SIMP =
     6.9  struct
    6.10  
    6.11  local open Simp_data in
    6.12 @@ -74,12 +74,12 @@
    6.13    Similar to match_from_nat_tac, but the net does not contain numbers;
    6.14    rewrite rules are not ordered.*)
    6.15  fun net_tac net =
    6.16 -  SUBGOAL(fn (prem,i) => 
    6.17 +  SUBGOAL(fn (prem,i) =>
    6.18            resolve_tac (Net.unify_term net (Logic.strip_assums_concl prem)) i);
    6.19  
    6.20  (*match subgoal i against possible theorems indexed by lhs in the net*)
    6.21  fun lhs_net_tac net =
    6.22 -  SUBGOAL(fn (prem,i) => 
    6.23 +  SUBGOAL(fn (prem,i) =>
    6.24            biresolve_tac (Net.unify_term net
    6.25                         (lhs_of (Logic.strip_assums_concl prem))) i);
    6.26  
    6.27 @@ -110,7 +110,7 @@
    6.28  
    6.29  (*Get the norm constants from norm_thms*)
    6.30  val norms =
    6.31 -  let fun norm thm = 
    6.32 +  let fun norm thm =
    6.33        case lhs_of(concl_of thm) of
    6.34            Const(n,_)$_ => n
    6.35          | _ => error "No constant in lhs of a norm_thm"
    6.36 @@ -144,7 +144,7 @@
    6.37  (**** Adding "NORM" tags ****)
    6.38  
    6.39  (*get name of the constant from conclusion of a congruence rule*)
    6.40 -fun cong_const cong = 
    6.41 +fun cong_const cong =
    6.42      case head_of (lhs_of (concl_of cong)) of
    6.43          Const(c,_) => c
    6.44        | _ => ""                 (*a placeholder distinct from const names*);
    6.45 @@ -156,9 +156,9 @@
    6.46  fun add_hidden_vars ccs =
    6.47    let fun add_hvars tm hvars = case tm of
    6.48                Abs(_,_,body) => OldTerm.add_term_vars(body,hvars)
    6.49 -            | _$_ => let val (f,args) = strip_comb tm 
    6.50 +            | _$_ => let val (f,args) = strip_comb tm
    6.51                       in case f of
    6.52 -                            Const(c,T) => 
    6.53 +                            Const(c,T) =>
    6.54                                  if member (op =) ccs c
    6.55                                  then fold_rev add_hvars args hvars
    6.56                                  else OldTerm.add_term_vars (tm, hvars)
    6.57 @@ -202,13 +202,13 @@
    6.58      val hvs = map (#1 o dest_Var) hvars
    6.59      val refl1_tac = refl_tac 1
    6.60      fun norm_step_tac st = st |>
    6.61 -	 (case head_of(rhs_of_eq 1 st) of
    6.62 -	    Var(ixn,_) => if ixn mem hvs then refl1_tac
    6.63 -			  else resolve_tac normI_thms 1 ORELSE refl1_tac
    6.64 -	  | Const _ => resolve_tac normI_thms 1 ORELSE
    6.65 -		       resolve_tac congs 1 ORELSE refl1_tac
    6.66 -	  | Free _ => resolve_tac congs 1 ORELSE refl1_tac
    6.67 -	  | _ => refl1_tac)
    6.68 +         (case head_of(rhs_of_eq 1 st) of
    6.69 +            Var(ixn,_) => if ixn mem hvs then refl1_tac
    6.70 +                          else resolve_tac normI_thms 1 ORELSE refl1_tac
    6.71 +          | Const _ => resolve_tac normI_thms 1 ORELSE
    6.72 +                       resolve_tac congs 1 ORELSE refl1_tac
    6.73 +          | Free _ => resolve_tac congs 1 ORELSE refl1_tac
    6.74 +          | _ => refl1_tac)
    6.75      val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac
    6.76      val SOME(thm'',_) = Seq.pull(add_norm_tac thm')
    6.77  in thm'' end;
    6.78 @@ -246,9 +246,9 @@
    6.79  (** Insertion of congruences and rewrites **)
    6.80  
    6.81  (*insert a thm in a thm net*)
    6.82 -fun insert_thm_warn th net = 
    6.83 +fun insert_thm_warn th net =
    6.84    Net.insert_term Thm.eq_thm_prop (concl_of th, th) net
    6.85 -  handle Net.INSERT => 
    6.86 +  handle Net.INSERT =>
    6.87      (writeln ("Duplicate rewrite or congruence rule:\n" ^
    6.88          Display.string_of_thm_without_context th); net);
    6.89  
    6.90 @@ -272,9 +272,9 @@
    6.91  (** Deletion of congruences and rewrites **)
    6.92  
    6.93  (*delete a thm from a thm net*)
    6.94 -fun delete_thm_warn th net = 
    6.95 +fun delete_thm_warn th net =
    6.96    Net.delete_term Thm.eq_thm_prop (concl_of th, th) net
    6.97 -  handle Net.DELETE => 
    6.98 +  handle Net.DELETE =>
    6.99      (writeln ("No such rewrite or congruence rule:\n" ^
   6.100          Display.string_of_thm_without_context th); net);
   6.101  
   6.102 @@ -337,17 +337,17 @@
   6.103      in find_if(tm,0) end;
   6.104  
   6.105  fun IF1_TAC cong_tac i =
   6.106 -    let fun seq_try (ifth::ifths,ifc::ifcs) thm = 
   6.107 +    let fun seq_try (ifth::ifths,ifc::ifcs) thm =
   6.108                  (COND (if_rewritable ifc i) (DETERM(rtac ifth i))
   6.109                          (seq_try(ifths,ifcs))) thm
   6.110                | seq_try([],_) thm = no_tac thm
   6.111          and try_rew thm = (seq_try(case_rews,case_consts) ORELSE one_subt) thm
   6.112          and one_subt thm =
   6.113                  let val test = has_fewer_prems (nprems_of thm + 1)
   6.114 -                    fun loop thm = 
   6.115 -			COND test no_tac
   6.116 +                    fun loop thm =
   6.117 +                        COND test no_tac
   6.118                            ((try_rew THEN DEPTH_FIRST test (refl_tac i))
   6.119 -			   ORELSE (refl_tac i THEN loop)) thm
   6.120 +                           ORELSE (refl_tac i THEN loop)) thm
   6.121                  in (cong_tac THEN loop) thm end
   6.122      in COND (may_match(case_consts,i)) try_rew no_tac end;
   6.123  
   6.124 @@ -381,12 +381,12 @@
   6.125  
   6.126  (*print lhs of conclusion of subgoal i*)
   6.127  fun pr_goal_lhs i st =
   6.128 -    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) 
   6.129 +    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st)
   6.130               (lhs_of (prepare_goal i st)));
   6.131  
   6.132  (*print conclusion of subgoal i*)
   6.133  fun pr_goal_concl i st =
   6.134 -    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) (prepare_goal i st)) 
   6.135 +    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) (prepare_goal i st))
   6.136  
   6.137  (*print subgoals i to j (inclusive)*)
   6.138  fun pr_goals (i,j) st =
   6.139 @@ -439,7 +439,7 @@
   6.140          then writeln (cat_lines
   6.141            ("Adding rewrites:" :: map Display.string_of_thm_without_context new_rws))
   6.142          else ();
   6.143 -        (ss,thm,anet',anet::ats,cs) 
   6.144 +        (ss,thm,anet',anet::ats,cs)
   6.145      end;
   6.146  
   6.147  fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of
   6.148 @@ -492,7 +492,7 @@
   6.149  
   6.150  fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
   6.151  let val cong_tac = net_tac cong_net
   6.152 -in fn i => 
   6.153 +in fn i =>
   6.154      (fn thm =>
   6.155       if i <= 0 orelse nprems_of thm < i then Seq.empty
   6.156       else Seq.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
     7.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Sat Aug 29 10:50:04 2009 +0200
     7.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Sat Aug 29 12:01:25 2009 +0200
     7.3 @@ -241,7 +241,7 @@
     7.4  proof (induct n)
     7.5    case 0 show ?case by simp
     7.6  next
     7.7 -  case Suc thus ?case by (simp add: add_assoc) 
     7.8 +  case Suc thus ?case by (simp add: add_assoc)
     7.9  qed
    7.10  
    7.11  lemma natsum_cong [cong]:
    7.12 @@ -269,21 +269,21 @@
    7.13  
    7.14  ML {*
    7.15    local
    7.16 -    val lhss = 
    7.17 +    val lhss =
    7.18          ["t + u::'a::ring",
    7.19 -	 "t - u::'a::ring",
    7.20 -	 "t * u::'a::ring",
    7.21 -	 "- t::'a::ring"];
    7.22 -    fun proc ss t = 
    7.23 +         "t - u::'a::ring",
    7.24 +         "t * u::'a::ring",
    7.25 +         "- t::'a::ring"];
    7.26 +    fun proc ss t =
    7.27        let val rew = Goal.prove (Simplifier.the_context ss) [] []
    7.28              (HOLogic.mk_Trueprop
    7.29                (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
    7.30                  (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)
    7.31              |> mk_meta_eq;
    7.32            val (t', u) = Logic.dest_equals (Thm.prop_of rew);
    7.33 -      in if t' aconv u 
    7.34 +      in if t' aconv u
    7.35          then NONE
    7.36 -        else SOME rew 
    7.37 +        else SOME rew
    7.38      end;
    7.39    in
    7.40      val ring_simproc = Simplifier.simproc @{theory} "ring" lhss (K proc);
    7.41 @@ -305,7 +305,7 @@
    7.42  declare one_not_zero [simp]
    7.43  
    7.44  lemma zero_not_one [simp]:
    7.45 -  "0 ~= (1::'a::domain)" 
    7.46 +  "0 ~= (1::'a::domain)"
    7.47  by (rule not_sym) simp
    7.48  
    7.49  lemma integral_iff: (* not by default a simp rule! *)
    7.50 @@ -322,7 +322,7 @@
    7.51  *)
    7.52  (*
    7.53  lemma bug: "(b::'a::ring) - (b - a) = a" by simp
    7.54 -   simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" 
    7.55 +   simproc for rings cannot prove "(a::'a::ring) - (a - b) = b"
    7.56  *)
    7.57  lemma m_lcancel:
    7.58    assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
    7.59 @@ -330,8 +330,8 @@
    7.60    assume eq: "a * b = a * c"
    7.61    then have "a * (b - c) = 0" by simp
    7.62    then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
    7.63 -  with prem have "b - c = 0" by auto 
    7.64 -  then have "b = b - (b - c)" by simp 
    7.65 +  with prem have "b - c = 0" by auto
    7.66 +  then have "b = b - (b - c)" by simp
    7.67    also have "b - (b - c) = c" by simp
    7.68    finally show "b = c" .
    7.69  next
    7.70 @@ -386,7 +386,7 @@
    7.71  qed
    7.72  
    7.73  
    7.74 -lemma unit_mult: 
    7.75 +lemma unit_mult:
    7.76    "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1"
    7.77    apply (unfold dvd_def)
    7.78    apply clarify