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