merged;
authorwenzelm
Fri Jun 29 22:14:33 2018 +0200 (11 months ago)
changeset 68547549a4992222f
parent 68535 4d09df93d1a2
parent 68546 34d732a83767
child 68548 a22540ac7052
child 68549 bbc742358156
merged;
CONTRIBUTORS
NEWS
src/HOL/Fields.thy
src/HOL/Rat.thy
     1.1 --- a/ANNOUNCE	Fri Jun 29 15:22:30 2018 +0100
     1.2 +++ b/ANNOUNCE	Fri Jun 29 22:14:33 2018 +0200
     1.3 @@ -4,9 +4,25 @@
     1.4  Isabelle2018 is now available.
     1.5  
     1.6  This version introduces many changes over Isabelle2017: see the NEWS
     1.7 -file for further details. Some notable points:
     1.8 +file for further details. Here are the main points:
     1.9 +
    1.10 +* Improved infix notation within terms.
    1.11 +
    1.12 +* Improved syntax for formal comments, within terms and other languages.
    1.13 +
    1.14 +* Improved management of ROOT files and session-qualified theories.
    1.15 +
    1.16 +* Various improvements of document preparation.
    1.17  
    1.18 -* FIXME.
    1.19 +* Many Isabelle/jEdit improvements, including semantic IDE for Bibtex.
    1.20 +
    1.21 +* Numerous HOL library improvements, including HOL-Algebra.
    1.22 +
    1.23 +* Substantial additions to HOL-Analysis.
    1.24 +
    1.25 +* Isabelle server for reactive communication with other programs.
    1.26 +
    1.27 +* More uniform 64-bit platform support: smaller Isabelle application.
    1.28  
    1.29  
    1.30  You may get Isabelle2018 from the following mirror sites:
     2.1 --- a/Admin/Release/CHECKLIST	Fri Jun 29 15:22:30 2018 +0100
     2.2 +++ b/Admin/Release/CHECKLIST	Fri Jun 29 22:14:33 2018 +0200
     2.3 @@ -5,6 +5,14 @@
     2.4  
     2.5  - check Admin/components;
     2.6  
     2.7 +- test "isabelle dump -l Pure ZF";
     2.8 +
     2.9 +- test "isabelle -o export_theory -f ZF";
    2.10 +
    2.11 +- test "isabelle server" according to "system" manual;
    2.12 +
    2.13 +- test Isabelle/VSCode;
    2.14 +
    2.15  - test Isabelle/jEdit: print buffer
    2.16  
    2.17  - test "#!/usr/bin/env isabelle_scala_script";
     3.1 --- a/CONTRIBUTORS	Fri Jun 29 15:22:30 2018 +0100
     3.2 +++ b/CONTRIBUTORS	Fri Jun 29 22:14:33 2018 +0200
     3.3 @@ -15,6 +15,10 @@
     3.4  * June 2018: Wenda Li
     3.5    New/strengthened results involving analysis, topology, etc.
     3.6  
     3.7 +* May/June 2018: Makarius Wenzel
     3.8 +  System infrastructure to export blobs as theory presentation, and to dump
     3.9 +  PIDE database content in batch mode.
    3.10 +
    3.11  * May 2018: Manuel Eberl
    3.12    Landau symbols and asymptotic equivalence (moved from the AFP).
    3.13  
     4.1 --- a/NEWS	Fri Jun 29 15:22:30 2018 +0100
     4.2 +++ b/NEWS	Fri Jun 29 22:14:33 2018 +0200
     4.3 @@ -19,6 +19,11 @@
     4.4  FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
     4.5  formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
     4.6  
     4.7 +* Global facts need to be closed: no free variables, no hypotheses, no
     4.8 +pending sort hypotheses. Rare INCOMPATIBILITY: sort hypotheses can be
     4.9 +allowed via "declare [[pending_shyps]]" in the global theory context,
    4.10 +but it should be reset to false afterwards.
    4.11 +
    4.12  * Marginal comments need to be written exclusively in the new-style form
    4.13  "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
    4.14  supported. INCOMPATIBILITY, use the command-line tool "isabelle
    4.15 @@ -31,13 +36,13 @@
    4.16  * The "op <infix-op>" syntax for infix operators has been replaced by
    4.17  "(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to
    4.18  be a space between the "*" and the corresponding parenthesis.
    4.19 -INCOMPATIBILITY.
    4.20 -There is an Isabelle tool "update_op" that converts theory and ML files
    4.21 -to the new syntax. Because it is based on regular expression matching,
    4.22 -the result may need a bit of manual postprocessing. Invoking "isabelle
    4.23 -update_op" converts all files in the current directory (recursively).
    4.24 -In case you want to exclude conversion of ML files (because the tool
    4.25 -frequently also converts ML's "op" syntax), use option "-m".
    4.26 +INCOMPATIBILITY, use the command-line tool "isabelle update_op" to
    4.27 +convert theory and ML files to the new syntax. Because it is based on
    4.28 +regular expression matching, the result may need a bit of manual
    4.29 +postprocessing. Invoking "isabelle update_op" converts all files in the
    4.30 +current directory (recursively). In case you want to exclude conversion
    4.31 +of ML files (because the tool frequently also converts ML's "op"
    4.32 +syntax), use option "-m".
    4.33  
    4.34  * Theory header 'abbrevs' specifications need to be separated by 'and'.
    4.35  INCOMPATIBILITY.
    4.36 @@ -80,11 +85,15 @@
    4.37    - option -A specifies an alternative ancestor session for options -R
    4.38      and -S
    4.39  
    4.40 +  - option -i includes additional sessions into the name-space of
    4.41 +    theories
    4.42 +
    4.43    Examples:
    4.44      isabelle jedit -R HOL-Number_Theory
    4.45      isabelle jedit -R HOL-Number_Theory -A HOL
    4.46      isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
    4.47      isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
    4.48 +    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis -i CryptHOL
    4.49  
    4.50  * PIDE markup for session ROOT files: allows to complete session names,
    4.51  follow links to theories and document files etc.
    4.52 @@ -119,14 +128,14 @@
    4.53  plain-text document draft. Both are available via the menu "Plugins /
    4.54  Isabelle".
    4.55  
    4.56 -* Bibtex database files (.bib) are semantically checked.
    4.57 -
    4.58  * When loading text files, the Isabelle symbols encoding UTF-8-Isabelle
    4.59  is only used if there is no conflict with existing Unicode sequences in
    4.60  the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle
    4.61  symbols remain in literal \<symbol> form. This avoids accidental loss of
    4.62  Unicode content when saving the file.
    4.63  
    4.64 +* Bibtex database files (.bib) are semantically checked.
    4.65 +
    4.66  * Update to jedit-5.5.0, the latest release.
    4.67  
    4.68  
    4.69 @@ -198,6 +207,12 @@
    4.70  Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
    4.71  object-logic equality or equivalence.
    4.72  
    4.73 +
    4.74 +*** Pure ***
    4.75 +
    4.76 +* The inner syntax category "sort" now includes notation "_" for the
    4.77 +dummy sort: it is effectively ignored in type-inference.
    4.78 +
    4.79  * Rewrites clauses (keyword 'rewrites') were moved into the locale
    4.80  expression syntax, where they are part of locale instances. In
    4.81  interpretation commands rewrites clauses now need to occur before 'for'
    4.82 @@ -209,17 +224,11 @@
    4.83  locale instances where the qualifier's sole purpose is avoiding
    4.84  duplicate constant declarations.
    4.85  
    4.86 -* Proof method 'simp' now supports a new modifier 'flip:' followed by a list
    4.87 -of theorems. Each of these theorems is removed from the simpset
    4.88 -(without warning if it is not there) and the symmetric version of the theorem
    4.89 -(i.e. lhs and rhs exchanged) is added to the simpset.
    4.90 -For 'auto' and friends the modifier is "simp flip:".
    4.91 -
    4.92 -
    4.93 -*** Pure ***
    4.94 -
    4.95 -* The inner syntax category "sort" now includes notation "_" for the
    4.96 -dummy sort: it is effectively ignored in type-inference.
    4.97 +* Proof method "simp" now supports a new modifier "flip:" followed by a
    4.98 +list of theorems. Each of these theorems is removed from the simpset
    4.99 +(without warning if it is not there) and the symmetric version of the
   4.100 +theorem (i.e. lhs and rhs exchanged) is added to the simpset. For "auto"
   4.101 +and friends the modifier is "simp flip:".
   4.102  
   4.103  
   4.104  *** HOL ***
   4.105 @@ -382,12 +391,12 @@
   4.106  * Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new
   4.107  infix/prefix notation.
   4.108  
   4.109 -* Session HOL-Algebra: Revamped with much new material.
   4.110 -The set of isomorphisms between two groups is now denoted iso rather than iso_set.
   4.111 -INCOMPATIBILITY.
   4.112 -
   4.113 -* Session HOL-Analysis: the Arg function now respects the same interval as
   4.114 -Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi. 
   4.115 +* Session HOL-Algebra: revamped with much new material. The set of
   4.116 +isomorphisms between two groups is now denoted iso rather than iso_set.
   4.117 +INCOMPATIBILITY.
   4.118 +
   4.119 +* Session HOL-Analysis: the Arg function now respects the same interval
   4.120 +as Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi.
   4.121  INCOMPATIBILITY.
   4.122  
   4.123  * Session HOL-Analysis: the functions zorder, zer_poly, porder and pol_poly have been redefined. 
   4.124 @@ -398,10 +407,9 @@
   4.125  Riemann mapping theorem, the Vitali covering theorem,
   4.126  change-of-variables results for integration and measures.
   4.127  
   4.128 -* Session HOL-Types_To_Sets: more tool support
   4.129 -(unoverload_type combines internalize_sorts and unoverload) and larger
   4.130 -experimental application (type based linear algebra transferred to linear
   4.131 -algebra on subspaces).
   4.132 +* Session HOL-Types_To_Sets: more tool support (unoverload_type combines
   4.133 +internalize_sorts and unoverload) and larger experimental application
   4.134 +(type based linear algebra transferred to linear algebra on subspaces).
   4.135  
   4.136  
   4.137  *** ML ***
     5.1 --- a/src/Doc/Implementation/Logic.thy	Fri Jun 29 15:22:30 2018 +0100
     5.2 +++ b/src/Doc/Implementation/Logic.thy	Fri Jun 29 22:14:33 2018 +0200
     5.3 @@ -862,9 +862,13 @@
     5.4  class empty =
     5.5    assumes bad: "\<And>(x::'a) y. x \<noteq> y"
     5.6  
     5.7 +declare [[pending_shyps]]
     5.8 +
     5.9  theorem (in empty) false: False
    5.10    using bad by blast
    5.11  
    5.12 +declare [[pending_shyps = false]]
    5.13 +
    5.14  ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
    5.15  
    5.16  text \<open>
     6.1 --- a/src/Doc/JEdit/JEdit.thy	Fri Jun 29 15:22:30 2018 +0100
     6.2 +++ b/src/Doc/JEdit/JEdit.thy	Fri Jun 29 22:14:33 2018 +0200
     6.3 @@ -237,6 +237,7 @@
     6.4      -b           build only
     6.5      -d DIR       include session directory
     6.6      -f           fresh build
     6.7 +    -i NAME      include session in name-space of theories
     6.8      -j OPTION    add jEdit runtime option
     6.9                   (default $JEDIT_OPTIONS)
    6.10      -l NAME      logic image name
    6.11 @@ -266,6 +267,9 @@
    6.12    ancestor session for options \<^verbatim>\<open>-R\<close> and \<^verbatim>\<open>-S\<close>: this allows to restructure the
    6.13    hierarchy of session images on the spot.
    6.14  
    6.15 +  The \<^verbatim>\<open>-i\<close> option includes additional sessions into the name-space of
    6.16 +  theories: multiple occurrences are possible.
    6.17 +
    6.18    The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.
    6.19    Note that the system option @{system_option_ref jedit_print_mode} allows to
    6.20    do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close> dialog of
     7.1 --- a/src/Doc/System/Environment.thy	Fri Jun 29 15:22:30 2018 +0100
     7.2 +++ b/src/Doc/System/Environment.thy	Fri Jun 29 22:14:33 2018 +0200
     7.3 @@ -407,6 +407,7 @@
     7.4  
     7.5    Options are:
     7.6      -d DIR       include session directory
     7.7 +    -i NAME      include session in name-space of theories
     7.8      -l NAME      logic session name (default ISABELLE_LOGIC)
     7.9      -m MODE      add print mode for output
    7.10      -n           no build of session image on startup
    7.11 @@ -421,6 +422,9 @@
    7.12    Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
    7.13    checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
    7.14  
    7.15 +  Option \<^verbatim>\<open>-i\<close> includes additional sessions into the name-space of theories:
    7.16 +  multiple occurrences are possible.
    7.17 +
    7.18    Option \<^verbatim>\<open>-r\<close> indicates a bootstrap from the raw Poly/ML system, which is
    7.19    relevant for Isabelle/Pure development.
    7.20  
     8.1 --- a/src/FOL/ex/Miniscope.thy	Fri Jun 29 15:22:30 2018 +0100
     8.2 +++ b/src/FOL/ex/Miniscope.thy	Fri Jun 29 22:14:33 2018 +0200
     8.3 @@ -17,14 +17,19 @@
     8.4  
     8.5  subsubsection \<open>de Morgan laws\<close>
     8.6  
     8.7 -lemma demorgans:
     8.8 +lemma demorgans1:
     8.9    "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"
    8.10    "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q"
    8.11    "\<not> \<not> P \<longleftrightarrow> P"
    8.12 +  by blast+
    8.13 +
    8.14 +lemma demorgans2:
    8.15    "\<And>P. \<not> (\<forall>x. P(x)) \<longleftrightarrow> (\<exists>x. \<not> P(x))"
    8.16    "\<And>P. \<not> (\<exists>x. P(x)) \<longleftrightarrow> (\<forall>x. \<not> P(x))"
    8.17    by blast+
    8.18  
    8.19 +lemmas demorgans = demorgans1 demorgans2
    8.20 +
    8.21  (*** Removal of --> and <-> (positive and negative occurrences) ***)
    8.22  (*Last one is important for computing a compact CNF*)
    8.23  lemma nnf_simps:
     9.1 --- a/src/HOL/Euclidean_Division.thy	Fri Jun 29 15:22:30 2018 +0100
     9.2 +++ b/src/HOL/Euclidean_Division.thy	Fri Jun 29 22:14:33 2018 +0200
     9.3 @@ -1638,7 +1638,7 @@
     9.4        by (simp only: *, simp only: l q divide_int_unfold)
     9.5          (auto simp add: sgn_mult sgn_0_0 sgn_1_pos algebra_simps dest: dvd_imp_le)
     9.6    qed
     9.7 -qed (use mult_le_mono2 [of 1] in \<open>auto simp add: division_segment_int_def not_le sign_simps abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
     9.8 +qed (use mult_le_mono2 [of 1] in \<open>auto simp add: division_segment_int_def not_le zero_less_mult_iff mult_less_0_iff abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
     9.9  
    9.10  end
    9.11  
    10.1 --- a/src/HOL/Fields.thy	Fri Jun 29 15:22:30 2018 +0100
    10.2 +++ b/src/HOL/Fields.thy	Fri Jun 29 22:14:33 2018 +0200
    10.3 @@ -843,10 +843,6 @@
    10.4  of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close> because the former can lead to case
    10.5  explosions.\<close>
    10.6  
    10.7 -lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
    10.8 -
    10.9 -lemmas (in -) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
   10.10 -
   10.11  (* Only works once linear arithmetic is installed:
   10.12  text{*An example:*}
   10.13  lemma fixes a b c d e f :: "'a::linordered_field"
    11.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Fri Jun 29 15:22:30 2018 +0100
    11.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Fri Jun 29 22:14:33 2018 +0200
    11.3 @@ -457,7 +457,7 @@
    11.4    hence "\<exists>(v::'a) (u::'a) SKF\<^sub>7::'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^sub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^sub>7 (u * v))\<bar>)"
    11.5      by (metis mult_left_mono)
    11.6    then show "\<exists>ca::'a. \<forall>x::'b. inverse \<bar>c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
    11.7 -    using A2 F4 by (metis F1 \<open>0 < \<bar>inverse c\<bar>\<close> linordered_field_class.sign_simps(23) mult_le_cancel_left_pos)
    11.8 +    using A2 F4 by (metis F1 \<open>0 < \<bar>inverse c\<bar>\<close> mult.assoc mult_le_cancel_left_pos)
    11.9  qed
   11.10  
   11.11  lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) <= O(f)"
    12.1 --- a/src/HOL/Num.thy	Fri Jun 29 15:22:30 2018 +0100
    12.2 +++ b/src/HOL/Num.thy	Fri Jun 29 22:14:33 2018 +0200
    12.3 @@ -1282,14 +1282,20 @@
    12.4    numeral for 1 reduces the number of special cases.
    12.5  \<close>
    12.6  
    12.7 -lemma mult_1s:
    12.8 +lemma mult_1s_semiring_numeral:
    12.9    "Numeral1 * a = a"
   12.10    "a * Numeral1 = a"
   12.11 +  for a :: "'a::semiring_numeral"
   12.12 +  by simp_all
   12.13 +
   12.14 +lemma mult_1s_ring_1:
   12.15    "- Numeral1 * b = - b"
   12.16    "b * - Numeral1 = - b"
   12.17 -  for a :: "'a::semiring_numeral" and b :: "'b::ring_1"
   12.18 +  for b :: "'a::ring_1"
   12.19    by simp_all
   12.20  
   12.21 +lemmas mult_1s = mult_1s_semiring_numeral mult_1s_ring_1
   12.22 +
   12.23  setup \<open>
   12.24    Reorient_Proc.add
   12.25      (fn Const (@{const_name numeral}, _) $ _ => true
   12.26 @@ -1385,13 +1391,20 @@
   12.27    "- numeral v + (- numeral w + y) = (- numeral(v + w) + y)"
   12.28    by (simp_all add: add.assoc [symmetric])
   12.29  
   12.30 -lemma mult_numeral_left [simp]:
   12.31 +lemma mult_numeral_left_semiring_numeral:
   12.32    "numeral v * (numeral w * z) = (numeral(v * w) * z :: 'a::semiring_numeral)"
   12.33 -  "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
   12.34 -  "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
   12.35 -  "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"
   12.36 +  by (simp add: mult.assoc [symmetric])
   12.37 +
   12.38 +lemma mult_numeral_left_ring_1:
   12.39 +  "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'a::ring_1)"
   12.40 +  "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'a::ring_1)"
   12.41 +  "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'a::ring_1)"
   12.42    by (simp_all add: mult.assoc [symmetric])
   12.43  
   12.44 +lemmas mult_numeral_left [simp] =
   12.45 +  mult_numeral_left_semiring_numeral
   12.46 +  mult_numeral_left_ring_1
   12.47 +
   12.48  hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec
   12.49  
   12.50  
    13.1 --- a/src/HOL/Rat.thy	Fri Jun 29 15:22:30 2018 +0100
    13.2 +++ b/src/HOL/Rat.thy	Fri Jun 29 22:14:33 2018 +0200
    13.3 @@ -529,6 +529,10 @@
    13.4  
    13.5  end
    13.6  
    13.7 +lemmas (in linordered_field) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
    13.8 +lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
    13.9 +
   13.10 +
   13.11  instantiation rat :: distrib_lattice
   13.12  begin
   13.13  
    14.1 --- a/src/Pure/Isar/attrib.ML	Fri Jun 29 15:22:30 2018 +0100
    14.2 +++ b/src/Pure/Isar/attrib.ML	Fri Jun 29 22:14:33 2018 +0200
    14.3 @@ -591,6 +591,7 @@
    14.4    register_config ML_Options.exception_trace_raw #>
    14.5    register_config ML_Options.exception_debugger_raw #>
    14.6    register_config ML_Options.debugger_raw #>
    14.7 +  register_config Global_Theory.pending_shyps_raw #>
    14.8    register_config Proof_Context.show_abbrevs_raw #>
    14.9    register_config Goal_Display.goals_limit_raw #>
   14.10    register_config Goal_Display.show_main_goal_raw #>
    15.1 --- a/src/Pure/ML/ml_console.scala	Fri Jun 29 15:22:30 2018 +0100
    15.2 +++ b/src/Pure/ML/ml_console.scala	Fri Jun 29 22:14:33 2018 +0200
    15.3 @@ -15,6 +15,7 @@
    15.4    {
    15.5      Command_Line.tool {
    15.6        var dirs: List[Path] = Nil
    15.7 +      var include_sessions: List[String] = Nil
    15.8        var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
    15.9        var modes: List[String] = Nil
   15.10        var no_build = false
   15.11 @@ -27,6 +28,7 @@
   15.12  
   15.13    Options are:
   15.14      -d DIR       include session directory
   15.15 +    -i NAME      include session in name-space of theories
   15.16      -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
   15.17      -m MODE      add print mode for output
   15.18      -n           no build of session image on startup
   15.19 @@ -39,6 +41,7 @@
   15.20    quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
   15.21  """,
   15.22          "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   15.23 +        "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
   15.24          "l:" -> (arg => logic = arg),
   15.25          "m:" -> (arg => modes = arg :: modes),
   15.26          "n" -> (arg => no_build = true),
   15.27 @@ -69,7 +72,8 @@
   15.28            store = Some(Sessions.store(options, system_mode)),
   15.29            session_base =
   15.30              if (raw_ml_system) None
   15.31 -            else Some(Sessions.base_info(options, logic, dirs = dirs).check_base))
   15.32 +            else Some(Sessions.base_info(
   15.33 +              options, logic, dirs = dirs, include_sessions = include_sessions).check_base))
   15.34  
   15.35        val tty_loop = new TTY_Loop(process.stdin, process.stdout, Some(process.interrupt _))
   15.36        val process_result = Future.thread[Int]("process_result") {
    16.1 --- a/src/Pure/PIDE/document.ML	Fri Jun 29 15:22:30 2018 +0100
    16.2 +++ b/src/Pure/PIDE/document.ML	Fri Jun 29 22:14:33 2018 +0200
    16.3 @@ -735,8 +735,9 @@
    16.4                      segments = segments};
    16.5                  in
    16.6                    fn _ =>
    16.7 -                    (Thy_Info.apply_presentation presentation_context thy;
    16.8 -                     commit_consolidated node)
    16.9 +                    Exn.release
   16.10 +                      (Exn.capture (Thy_Info.apply_presentation presentation_context) thy
   16.11 +                        before commit_consolidated node)
   16.12                  end
   16.13                else fn _ => commit_consolidated node;
   16.14  
    17.1 --- a/src/Pure/Thy/export_theory.ML	Fri Jun 29 15:22:30 2018 +0100
    17.2 +++ b/src/Pure/Thy/export_theory.ML	Fri Jun 29 22:14:33 2018 +0200
    17.3 @@ -102,6 +102,12 @@
    17.4  
    17.5      (* axioms and facts *)
    17.6  
    17.7 +    val standard_prop_of =
    17.8 +      Thm.transfer thy #>
    17.9 +      Thm.check_hyps (Context.Theory thy) #>
   17.10 +      Drule.sort_constraint_intr_shyps #>
   17.11 +      Thm.full_prop_of;
   17.12 +
   17.13      val encode_props =
   17.14        let open XML.Encode Term_XML.Encode
   17.15        in triple (list (pair string sort)) (list (pair string typ)) (list term) end;
   17.16 @@ -114,7 +120,7 @@
   17.17        in encode_props (typargs, args, props') end;
   17.18  
   17.19      val export_axiom = export_props o single;
   17.20 -    val export_fact = export_props o Term_Subst.zero_var_indexes_list o map Thm.full_prop_of;
   17.21 +    val export_fact = export_props o Term_Subst.zero_var_indexes_list o map standard_prop_of;
   17.22  
   17.23      val _ =
   17.24        export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
    18.1 --- a/src/Pure/Thy/sessions.scala	Fri Jun 29 15:22:30 2018 +0100
    18.2 +++ b/src/Pure/Thy/sessions.scala	Fri Jun 29 22:14:33 2018 +0200
    18.3 @@ -461,7 +461,11 @@
    18.4      {
    18.5        val sel_sessions1 = session1 :: session :: include_sessions
    18.6        val select_sessions1 =
    18.7 -        if (session_focus) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1
    18.8 +        if (session_focus) {
    18.9 +          full_sessions1.check_sessions(sel_sessions1)
   18.10 +          full_sessions1.imports_descendants(sel_sessions1)
   18.11 +        }
   18.12 +        else sel_sessions1
   18.13        full_sessions1.selection(Selection(sessions = select_sessions1))
   18.14      }
   18.15  
   18.16 @@ -679,13 +683,16 @@
   18.17                }
   18.18            })
   18.19  
   18.20 +    def check_sessions(names: List[String])
   18.21 +    {
   18.22 +      val bad_sessions = SortedSet(names.filterNot(defined(_)): _*).toList
   18.23 +      if (bad_sessions.nonEmpty)
   18.24 +        error("Undefined session(s): " + commas_quote(bad_sessions))
   18.25 +    }
   18.26 +
   18.27      def selection(sel: Selection): Structure =
   18.28      {
   18.29 -      val bad_sessions =
   18.30 -        SortedSet((sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions).
   18.31 -          filterNot(defined(_)): _*).toList
   18.32 -      if (bad_sessions.nonEmpty)
   18.33 -        error("Undefined session(s): " + commas_quote(bad_sessions))
   18.34 +      check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
   18.35  
   18.36        val excluded = sel.excluded(build_graph).toSet
   18.37  
    19.1 --- a/src/Pure/Tools/dump.scala	Fri Jun 29 15:22:30 2018 +0100
    19.2 +++ b/src/Pure/Tools/dump.scala	Fri Jun 29 22:14:33 2018 +0200
    19.3 @@ -93,8 +93,8 @@
    19.4      system_mode: Boolean = false,
    19.5      selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
    19.6    {
    19.7 -    if (Build.build_logic(options, logic, progress = progress, dirs = dirs,
    19.8 -      system_mode = system_mode) != 0) error(logic + " FAILED")
    19.9 +    if (Build.build_logic(options, logic, build_heap = true, progress = progress,
   19.10 +      dirs = dirs, system_mode = system_mode) != 0) error(logic + " FAILED")
   19.11  
   19.12      val dump_options = make_options(options, aspects)
   19.13  
    20.1 --- a/src/Pure/drule.ML	Fri Jun 29 15:22:30 2018 +0100
    20.2 +++ b/src/Pure/drule.ML	Fri Jun 29 22:14:33 2018 +0200
    20.3 @@ -98,6 +98,8 @@
    20.4    val is_sort_constraint: term -> bool
    20.5    val sort_constraintI: thm
    20.6    val sort_constraint_eq: thm
    20.7 +  val sort_constraint_intr: indexname * sort -> thm -> thm
    20.8 +  val sort_constraint_intr_shyps: thm -> thm
    20.9    val with_subgoal: int -> (thm -> thm) -> thm -> thm
   20.10    val comp_no_flatten: thm * int -> int -> thm -> thm
   20.11    val rename_bvars: (string * string) list -> thm -> thm
   20.12 @@ -647,6 +649,26 @@
   20.13          (Thm.unvarify_global (Context.the_global_context ()) sort_constraintI)))
   20.14        (implies_intr_list [A, C] (Thm.assume A)));
   20.15  
   20.16 +val sort_constraint_eq' = Thm.symmetric sort_constraint_eq;
   20.17 +
   20.18 +fun sort_constraint_intr tvar thm =
   20.19 +  Thm.equal_elim
   20.20 +    (Thm.instantiate
   20.21 +      ([((("'a", 0), []), Thm.global_ctyp_of (Thm.theory_of_thm thm) (TVar tvar))],
   20.22 +       [((("A", 0), propT), Thm.cprop_of thm)])
   20.23 +      sort_constraint_eq') thm;
   20.24 +
   20.25 +fun sort_constraint_intr_shyps raw_thm =
   20.26 +  let val thm = Thm.strip_shyps raw_thm in
   20.27 +    (case Thm.extra_shyps thm of
   20.28 +      [] => thm
   20.29 +    | shyps =>
   20.30 +        let
   20.31 +          val names = Name.make_context (map #1 (Thm.fold_terms Term.add_tvar_names thm []));
   20.32 +          val constraints = map (rpair 0) (Name.invent names Name.aT (length shyps)) ~~ shyps;
   20.33 +        in Thm.strip_shyps (fold_rev sort_constraint_intr constraints thm) end)
   20.34 +  end;
   20.35 +
   20.36  end;
   20.37  
   20.38  
    21.1 --- a/src/Pure/global_theory.ML	Fri Jun 29 15:22:30 2018 +0100
    21.2 +++ b/src/Pure/global_theory.ML	Fri Jun 29 22:14:33 2018 +0200
    21.3 @@ -24,6 +24,8 @@
    21.4    val name_thm: bool -> bool -> string -> thm -> thm
    21.5    val name_thms: bool -> bool -> string -> thm list -> thm list
    21.6    val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
    21.7 +  val pending_shyps_raw: Config.raw
    21.8 +  val pending_shyps: bool Config.T
    21.9    val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
   21.10    val store_thm: binding * thm -> theory -> thm * theory
   21.11    val store_thm_open: binding * thm -> theory -> thm * theory
   21.12 @@ -128,16 +130,35 @@
   21.13  
   21.14  fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
   21.15  
   21.16 +val pending_shyps_raw = Config.declare ("pending_shyps", \<^here>) (K (Config.Bool false));
   21.17 +val pending_shyps = Config.bool pending_shyps_raw;
   21.18 +
   21.19  fun add_facts (b, fact) thy =
   21.20    let
   21.21      val full_name = Sign.full_name thy b;
   21.22      val pos = Binding.pos_of b;
   21.23 -    fun err msg =
   21.24 -      error ("Malformed global fact " ^ quote full_name ^ Position.here pos ^ "\n" ^ msg);
   21.25 -    fun check thm =
   21.26 -      ignore (Logic.unvarify_global (Term_Subst.zero_var_indexes (Thm.full_prop_of thm)))
   21.27 -        handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
   21.28 -    val arg = (b, Lazy.map_finished (tap (List.app check)) fact);
   21.29 +    fun check fact =
   21.30 +      fact |> map_index (fn (i, thm) =>
   21.31 +        let
   21.32 +          fun err msg =
   21.33 +            error ("Malformed global fact " ^
   21.34 +              quote (full_name ^
   21.35 +                (if length fact = 1 then "" else "(" ^ string_of_int (i + 1) ^ ")")) ^
   21.36 +              Position.here pos ^ "\n" ^ msg);
   21.37 +          val prop = Thm.plain_prop_of thm
   21.38 +            handle THM _ =>
   21.39 +              thm
   21.40 +              |> not (Config.get_global thy pending_shyps) ?
   21.41 +                  Thm.check_shyps (Proof_Context.init_global thy)
   21.42 +              |> Thm.check_hyps (Context.Theory thy)
   21.43 +              |> Thm.full_prop_of;
   21.44 +        in
   21.45 +          ignore (Logic.unvarify_global (Term_Subst.zero_var_indexes prop))
   21.46 +            handle TYPE (msg, _, _) => err msg
   21.47 +              | TERM (msg, _) => err msg
   21.48 +              | ERROR msg => err msg
   21.49 +        end);
   21.50 +    val arg = (b, Lazy.map_finished (tap check) fact);
   21.51    in
   21.52      thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
   21.53    end;
    22.1 --- a/src/Tools/VSCode/extension/README.md	Fri Jun 29 15:22:30 2018 +0100
    22.2 +++ b/src/Tools/VSCode/extension/README.md	Fri Jun 29 22:14:33 2018 +0200
    22.3 @@ -1,14 +1,15 @@
    22.4  # Isabelle Prover IDE support
    22.5  
    22.6  This extension connects VSCode to the Isabelle Prover IDE infrastructure: it
    22.7 -requires a repository version of Isabelle.
    22.8 +requires Isabelle2018.
    22.9  
   22.10  The implementation is centered around the VSCode Language Server protocol, but
   22.11  with many add-ons that are specific to VSCode and Isabelle/PIDE.
   22.12  
   22.13  See also:
   22.14  
   22.15 -  * <https://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode>
   22.16 +  * <https://isabelle.in.tum.de/website-Isabelle2018>
   22.17 +  * <https://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/Tools/VSCode>
   22.18    * <https://github.com/Microsoft/language-server-protocol>
   22.19  
   22.20  
   22.21 @@ -58,8 +59,8 @@
   22.22  
   22.23  ### Isabelle/VSCode Installation
   22.24  
   22.25 -  * Download a recent Isabelle development snapshot from
   22.26 -  <http://isabelle.in.tum.de/devel/release_snapshot>
   22.27 +  * Download Isabelle2018 from <https://isabelle.in.tum.de/website-Isabelle2018>
   22.28 +    or any of its mirror sites.
   22.29  
   22.30    * Unpack and run the main Isabelle/jEdit application as usual, to ensure that
   22.31    the logic image is built properly and Isabelle works as expected.
   22.32 @@ -68,7 +69,7 @@
   22.33  
   22.34    * Open the VSCode *Extensions* view and install the following:
   22.35  
   22.36 -      + *Isabelle*.
   22.37 +      + *Isabelle2018* (needs to fit to the underlying Isabelle release).
   22.38  
   22.39        + *Prettify Symbols Mode* (important for display of Isabelle symbols).
   22.40  
   22.41 @@ -89,17 +90,17 @@
   22.42  
   22.43        + Linux:
   22.44          ```
   22.45 -        "isabelle.home": "/home/makarius/Isabelle"
   22.46 +        "isabelle.home": "/home/makarius/Isabelle2018"
   22.47          ```
   22.48  
   22.49        + Mac OS X:
   22.50          ```
   22.51 -        "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle"
   22.52 +        "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle2018"
   22.53          ```
   22.54  
   22.55        + Windows:
   22.56          ```
   22.57 -        "isabelle.home": "C:\\Users\\makarius\\Isabelle"
   22.58 +        "isabelle.home": "C:\\Users\\makarius\\Isabelle2018"
   22.59          ```
   22.60  
   22.61    * Restart the VSCode application to ensure that all extensions are properly
    23.1 --- a/src/Tools/VSCode/extension/package.json	Fri Jun 29 15:22:30 2018 +0100
    23.2 +++ b/src/Tools/VSCode/extension/package.json	Fri Jun 29 22:14:33 2018 +0200
    23.3 @@ -1,6 +1,6 @@
    23.4  {
    23.5 -    "name": "isabelle",
    23.6 -    "displayName": "Isabelle",
    23.7 +    "name": "Isabelle2018",
    23.8 +    "displayName": "Isabelle2018",
    23.9      "description": "Isabelle Prover IDE",
   23.10      "keywords": [
   23.11          "theorem prover",
    24.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Fri Jun 29 15:22:30 2018 +0100
    24.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Jun 29 22:14:33 2018 +0200
    24.3 @@ -106,6 +106,7 @@
    24.4    echo "    -b           build only"
    24.5    echo "    -d DIR       include session directory"
    24.6    echo "    -f           fresh build"
    24.7 +  echo "    -i NAME      include session in name-space of theories"
    24.8    echo "    -j OPTION    add jEdit runtime option"
    24.9    echo "                 (default $JEDIT_OPTIONS)"
   24.10    echo "    -l NAME      logic session name"
   24.11 @@ -142,6 +143,7 @@
   24.12  JEDIT_LOGIC_ANCESTOR=""
   24.13  JEDIT_LOGIC_REQUIREMENTS=""
   24.14  JEDIT_LOGIC_FOCUS=""
   24.15 +JEDIT_INCLUDE_SESSIONS=""
   24.16  JEDIT_SESSION_DIRS=""
   24.17  JEDIT_LOGIC=""
   24.18  JEDIT_PRINT_MODE=""
   24.19 @@ -150,7 +152,7 @@
   24.20  function getoptions()
   24.21  {
   24.22    OPTIND=1
   24.23 -  while getopts "A:BFD:J:R:S:bd:fj:l:m:np:s" OPT
   24.24 +  while getopts "A:BFD:J:R:S:bd:fi:j:l:m:np:s" OPT
   24.25    do
   24.26      case "$OPT" in
   24.27        A)
   24.28 @@ -181,6 +183,13 @@
   24.29            JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
   24.30          fi
   24.31          ;;
   24.32 +      i)
   24.33 +        if [ -z "$JEDIT_INCLUDE_SESSIONS" ]; then
   24.34 +          JEDIT_INCLUDE_SESSIONS="$OPTARG"
   24.35 +        else
   24.36 +          JEDIT_INCLUDE_SESSIONS="$JEDIT_INCLUDE_SESSIONS:$OPTARG"
   24.37 +        fi
   24.38 +        ;;
   24.39        f)
   24.40          BUILD_JARS="jars_fresh"
   24.41          ;;
   24.42 @@ -413,7 +422,7 @@
   24.43  if [ "$BUILD_ONLY" = false ]
   24.44  then
   24.45    export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
   24.46 -    JEDIT_LOGIC_FOCUS JEDIT_PRINT_MODE JEDIT_BUILD_MODE
   24.47 +    JEDIT_LOGIC_FOCUS JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_BUILD_MODE
   24.48    export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
   24.49    classpath "$JEDIT_HOME/dist/jedit.jar"
   24.50    exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
    25.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Fri Jun 29 15:22:30 2018 +0100
    25.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Fri Jun 29 22:14:33 2018 +0200
    25.3 @@ -42,6 +42,8 @@
    25.4    def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR"))
    25.5    def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true"
    25.6    def logic_focus: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_FOCUS") == "true"
    25.7 +  def logic_include_sessions: List[String] =
    25.8 +    space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS"))
    25.9  
   25.10    def logic_info(options: Options): Option[Sessions.Info] =
   25.11      try {
   25.12 @@ -108,6 +110,7 @@
   25.13    def session_base_info(options: Options): Sessions.Base_Info =
   25.14      Sessions.base_info(options,
   25.15        dirs = JEdit_Sessions.session_dirs(),
   25.16 +      include_sessions = logic_include_sessions,
   25.17        session = logic_name(options),
   25.18        session_ancestor = logic_ancestor,
   25.19        session_requirements = logic_requirements,