--- a/NEWS Tue Sep 01 22:01:27 2020 +0100
+++ b/NEWS Tue Sep 01 22:01:42 2020 +0100
@@ -7,6 +7,13 @@
New in this Isabelle version
----------------------------
+*** General ***
+
+* Proof method "subst" is confined to the original subgoal range: its
+included distinct_subgoals_tac no longer affects unrelated subgoals.
+Rare INCOMPATIBILITY.
+
+
*** Isabelle/jEdit Prover IDE ***
* The jEdit status line includes a widget for Isabelle/ML heap usage,
--- a/etc/options Tue Sep 01 22:01:27 2020 +0100
+++ b/etc/options Tue Sep 01 22:01:42 2020 +0100
@@ -297,9 +297,6 @@
section "Theory Export"
-option export_document : bool = false
- -- "export document sources to Isabelle/Scala"
-
option export_theory : bool = false
-- "export theory content to Isabelle/Scala"
--- a/src/HOL/Hoare_Parallel/Graph.thy Tue Sep 01 22:01:27 2020 +0100
+++ b/src/HOL/Hoare_Parallel/Graph.thy Tue Sep 01 22:01:42 2020 +0100
@@ -168,9 +168,7 @@
prefer 2 apply arith
apply(drule_tac n = "Suc nata" in Compl_lemma)
apply clarify
- using [[linarith_split_limit = 0]]
- apply force
- using [[linarith_split_limit = 9]]
+ subgoal using [[linarith_split_limit = 0]] by force
apply(drule leI)
apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
apply(erule_tac x = "m - (Suc nata)" in allE)
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Sep 01 22:01:27 2020 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Sep 01 22:01:42 2020 +0100
@@ -451,10 +451,7 @@
"max_of_list (xs @ ys) = max (max_of_list xs) (max_of_list ys)"
apply (simp add: max_of_list_def)
apply (induct xs)
- apply simp
- using [[linarith_split_limit = 0]]
- apply simp
- apply arith
+ apply simp_all
done
--- a/src/Pure/PIDE/protocol.scala Tue Sep 01 22:01:27 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala Tue Sep 01 22:01:42 2020 +0100
@@ -12,7 +12,6 @@
/* markers for inlined messages */
val Loading_Theory_Marker = Protocol_Message.Marker("loading_theory")
- val Export_Marker = Protocol_Message.Marker("export")
val Meta_Info_Marker = Protocol_Message.Marker("meta_info")
val Command_Timing_Marker = Protocol_Message.Marker("command_timing")
val Theory_Timing_Marker = Protocol_Message.Marker("theory_timing")
@@ -200,30 +199,6 @@
def compound_name: String = isabelle.Export.compound_name(theory_name, name)
}
- object Marker
- {
- def unapply(line: String): Option[(Args, Path)] =
- line match {
- case Export_Marker(text) =>
- val props = XML.Decode.properties(YXML.parse_body(text))
- props match {
- case
- List(
- (Markup.SERIAL, Value.Long(serial)),
- (Markup.THEORY_NAME, theory_name),
- (Markup.NAME, name),
- (Markup.EXECUTABLE, Value.Boolean(executable)),
- (Markup.COMPRESS, Value.Boolean(compress)),
- (Markup.STRICT, Value.Boolean(strict)),
- (Markup.FILE, file)) if isabelle.Path.is_valid(file) =>
- val args = Args(None, serial, theory_name, name, executable, compress, strict)
- Some((args, isabelle.Path.explode(file)))
- case _ => None
- }
- case _ => None
- }
- }
-
def unapply(props: Properties.T): Option[Args] =
props match {
case
--- a/src/Pure/Thy/thy_info.ML Tue Sep 01 22:01:27 2020 +0100
+++ b/src/Pure/Thy/thy_info.ML Tue Sep 01 22:01:42 2020 +0100
@@ -68,10 +68,7 @@
let
val latex = Latex.isabelle_body (Context.theory_name thy) body;
val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
- val _ =
- if Options.bool options "export_document" then
- Export.export thy (Path.explode_binding0 "document.tex") (XML.blob output)
- else ();
+ val _ = Export.export thy (Path.explode_binding0 "document.tex") (XML.blob output);
val _ = if #enabled option then Present.theory_output thy output else ();
in () end
end));
--- a/src/Pure/Tools/dump.scala Tue Sep 01 22:01:27 2020 +0100
+++ b/src/Pure/Tools/dump.scala Tue Sep 01 22:01:42 2020 +0100
@@ -61,7 +61,7 @@
{ case args =>
for (entry <- args.snapshot.exports if entry.name == "document.tex")
args.write(Path.explode(entry.name), entry.uncompressed())
- }, options = List("export_document")),
+ }),
Aspect("theory", "foundational theory content",
{ case args =>
for {
--- a/src/Tools/eqsubst.ML Tue Sep 01 22:01:27 2020 +0100
+++ b/src/Tools/eqsubst.ML Tue Sep 01 22:01:42 2020 +0100
@@ -300,21 +300,17 @@
occurrences, but all earlier ones are skipped. Thus you can use [0] to
just find all rewrites. *)
-fun eqsubst_tac ctxt occs thms i st =
- let val nprems = Thm.nprems_of st in
- if nprems < i then Seq.empty else
+fun eqsubst_tac ctxt occs thms =
+ SELECT_GOAL
let
val thmseq = Seq.of_list thms;
- fun apply_occ occ st =
+ fun apply_occ_tac occ st =
thmseq |> Seq.maps (fn r =>
eqsubst_tac' ctxt
(skip_first_occs_search occ searchf_lr_unify_valid) r
- (i + (Thm.nprems_of st - nprems)) st);
+ (Thm.nprems_of st) st);
val sorted_occs = Library.sort (rev_order o int_ord) occs;
- in
- Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st)
- end
- end;
+ in Seq.EVERY (map apply_occ_tac sorted_occs) #> Seq.maps distinct_subgoals_tac end;
(* apply a substitution inside assumption j, keeps asm in the same place *)
@@ -391,22 +387,17 @@
fun skip_first_asm_occs_search searchf sinfo occ lhs =
skipto_skipseq occ (searchf sinfo lhs);
-fun eqsubst_asm_tac ctxt occs thms i st =
- let val nprems = Thm.nprems_of st in
- if nprems < i then Seq.empty
- else
- let
- val thmseq = Seq.of_list thms;
- fun apply_occ occ st =
- thmseq |> Seq.maps (fn r =>
- eqsubst_asm_tac' ctxt
- (skip_first_asm_occs_search searchf_lr_unify_valid) occ r
- (i + (Thm.nprems_of st - nprems)) st);
- val sorted_occs = Library.sort (rev_order o int_ord) occs;
- in
- Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st)
- end
- end;
+fun eqsubst_asm_tac ctxt occs thms =
+ SELECT_GOAL
+ let
+ val thmseq = Seq.of_list thms;
+ fun apply_occ_tac occ st =
+ thmseq |> Seq.maps (fn r =>
+ eqsubst_asm_tac' ctxt
+ (skip_first_asm_occs_search searchf_lr_unify_valid) occ r
+ (Thm.nprems_of st) st);
+ val sorted_occs = Library.sort (rev_order o int_ord) occs;
+ in Seq.EVERY (map apply_occ_tac sorted_occs) #> Seq.maps distinct_subgoals_tac end;
(* combination method that takes a flag (true indicates that subst
should be done to an assumption, false = apply to the conclusion of