--- a/ANNOUNCE Fri Jun 29 15:22:30 2018 +0100
+++ b/ANNOUNCE Fri Jun 29 22:14:33 2018 +0200
@@ -4,9 +4,25 @@
Isabelle2018 is now available.
This version introduces many changes over Isabelle2017: see the NEWS
-file for further details. Some notable points:
+file for further details. Here are the main points:
+
+* Improved infix notation within terms.
+
+* Improved syntax for formal comments, within terms and other languages.
+
+* Improved management of ROOT files and session-qualified theories.
+
+* Various improvements of document preparation.
-* FIXME.
+* Many Isabelle/jEdit improvements, including semantic IDE for Bibtex.
+
+* Numerous HOL library improvements, including HOL-Algebra.
+
+* Substantial additions to HOL-Analysis.
+
+* Isabelle server for reactive communication with other programs.
+
+* More uniform 64-bit platform support: smaller Isabelle application.
You may get Isabelle2018 from the following mirror sites:
--- a/Admin/Release/CHECKLIST Fri Jun 29 15:22:30 2018 +0100
+++ b/Admin/Release/CHECKLIST Fri Jun 29 22:14:33 2018 +0200
@@ -5,6 +5,14 @@
- check Admin/components;
+- test "isabelle dump -l Pure ZF";
+
+- test "isabelle -o export_theory -f ZF";
+
+- test "isabelle server" according to "system" manual;
+
+- test Isabelle/VSCode;
+
- test Isabelle/jEdit: print buffer
- test "#!/usr/bin/env isabelle_scala_script";
--- a/CONTRIBUTORS Fri Jun 29 15:22:30 2018 +0100
+++ b/CONTRIBUTORS Fri Jun 29 22:14:33 2018 +0200
@@ -15,6 +15,10 @@
* June 2018: Wenda Li
New/strengthened results involving analysis, topology, etc.
+* May/June 2018: Makarius Wenzel
+ System infrastructure to export blobs as theory presentation, and to dump
+ PIDE database content in batch mode.
+
* May 2018: Manuel Eberl
Landau symbols and asymptotic equivalence (moved from the AFP).
--- a/NEWS Fri Jun 29 15:22:30 2018 +0100
+++ b/NEWS Fri Jun 29 22:14:33 2018 +0200
@@ -19,6 +19,11 @@
FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
+* Global facts need to be closed: no free variables, no hypotheses, no
+pending sort hypotheses. Rare INCOMPATIBILITY: sort hypotheses can be
+allowed via "declare [[pending_shyps]]" in the global theory context,
+but it should be reset to false afterwards.
+
* Marginal comments need to be written exclusively in the new-style form
"\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
supported. INCOMPATIBILITY, use the command-line tool "isabelle
@@ -31,13 +36,13 @@
* The "op <infix-op>" syntax for infix operators has been replaced by
"(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to
be a space between the "*" and the corresponding parenthesis.
-INCOMPATIBILITY.
-There is an Isabelle tool "update_op" that converts theory and ML files
-to the new syntax. Because it is based on regular expression matching,
-the result may need a bit of manual postprocessing. Invoking "isabelle
-update_op" converts all files in the current directory (recursively).
-In case you want to exclude conversion of ML files (because the tool
-frequently also converts ML's "op" syntax), use option "-m".
+INCOMPATIBILITY, use the command-line tool "isabelle update_op" to
+convert theory and ML files to the new syntax. Because it is based on
+regular expression matching, the result may need a bit of manual
+postprocessing. Invoking "isabelle update_op" converts all files in the
+current directory (recursively). In case you want to exclude conversion
+of ML files (because the tool frequently also converts ML's "op"
+syntax), use option "-m".
* Theory header 'abbrevs' specifications need to be separated by 'and'.
INCOMPATIBILITY.
@@ -80,11 +85,15 @@
- option -A specifies an alternative ancestor session for options -R
and -S
+ - option -i includes additional sessions into the name-space of
+ theories
+
Examples:
isabelle jedit -R HOL-Number_Theory
isabelle jedit -R HOL-Number_Theory -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
+ isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis -i CryptHOL
* PIDE markup for session ROOT files: allows to complete session names,
follow links to theories and document files etc.
@@ -119,14 +128,14 @@
plain-text document draft. Both are available via the menu "Plugins /
Isabelle".
-* Bibtex database files (.bib) are semantically checked.
-
* When loading text files, the Isabelle symbols encoding UTF-8-Isabelle
is only used if there is no conflict with existing Unicode sequences in
the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle
symbols remain in literal \<symbol> form. This avoids accidental loss of
Unicode content when saving the file.
+* Bibtex database files (.bib) are semantically checked.
+
* Update to jedit-5.5.0, the latest release.
@@ -198,6 +207,12 @@
Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
object-logic equality or equivalence.
+
+*** Pure ***
+
+* The inner syntax category "sort" now includes notation "_" for the
+dummy sort: it is effectively ignored in type-inference.
+
* Rewrites clauses (keyword 'rewrites') were moved into the locale
expression syntax, where they are part of locale instances. In
interpretation commands rewrites clauses now need to occur before 'for'
@@ -209,17 +224,11 @@
locale instances where the qualifier's sole purpose is avoiding
duplicate constant declarations.
-* Proof method 'simp' now supports a new modifier 'flip:' followed by a list
-of theorems. Each of these theorems is removed from the simpset
-(without warning if it is not there) and the symmetric version of the theorem
-(i.e. lhs and rhs exchanged) is added to the simpset.
-For 'auto' and friends the modifier is "simp flip:".
-
-
-*** Pure ***
-
-* The inner syntax category "sort" now includes notation "_" for the
-dummy sort: it is effectively ignored in type-inference.
+* Proof method "simp" now supports a new modifier "flip:" followed by a
+list of theorems. Each of these theorems is removed from the simpset
+(without warning if it is not there) and the symmetric version of the
+theorem (i.e. lhs and rhs exchanged) is added to the simpset. For "auto"
+and friends the modifier is "simp flip:".
*** HOL ***
@@ -382,12 +391,12 @@
* Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new
infix/prefix notation.
-* Session HOL-Algebra: Revamped with much new material.
-The set of isomorphisms between two groups is now denoted iso rather than iso_set.
-INCOMPATIBILITY.
-
-* Session HOL-Analysis: the Arg function now respects the same interval as
-Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi.
+* Session HOL-Algebra: revamped with much new material. The set of
+isomorphisms between two groups is now denoted iso rather than iso_set.
+INCOMPATIBILITY.
+
+* Session HOL-Analysis: the Arg function now respects the same interval
+as Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi.
INCOMPATIBILITY.
* Session HOL-Analysis: the functions zorder, zer_poly, porder and pol_poly have been redefined.
@@ -398,10 +407,9 @@
Riemann mapping theorem, the Vitali covering theorem,
change-of-variables results for integration and measures.
-* Session HOL-Types_To_Sets: more tool support
-(unoverload_type combines internalize_sorts and unoverload) and larger
-experimental application (type based linear algebra transferred to linear
-algebra on subspaces).
+* Session HOL-Types_To_Sets: more tool support (unoverload_type combines
+internalize_sorts and unoverload) and larger experimental application
+(type based linear algebra transferred to linear algebra on subspaces).
*** ML ***
--- a/src/Doc/Implementation/Logic.thy Fri Jun 29 15:22:30 2018 +0100
+++ b/src/Doc/Implementation/Logic.thy Fri Jun 29 22:14:33 2018 +0200
@@ -862,9 +862,13 @@
class empty =
assumes bad: "\<And>(x::'a) y. x \<noteq> y"
+declare [[pending_shyps]]
+
theorem (in empty) false: False
using bad by blast
+declare [[pending_shyps = false]]
+
ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
text \<open>
--- a/src/Doc/JEdit/JEdit.thy Fri Jun 29 15:22:30 2018 +0100
+++ b/src/Doc/JEdit/JEdit.thy Fri Jun 29 22:14:33 2018 +0200
@@ -237,6 +237,7 @@
-b build only
-d DIR include session directory
-f fresh build
+ -i NAME include session in name-space of theories
-j OPTION add jEdit runtime option
(default $JEDIT_OPTIONS)
-l NAME logic image name
@@ -266,6 +267,9 @@
ancestor session for options \<^verbatim>\<open>-R\<close> and \<^verbatim>\<open>-S\<close>: this allows to restructure the
hierarchy of session images on the spot.
+ The \<^verbatim>\<open>-i\<close> option includes additional sessions into the name-space of
+ theories: multiple occurrences are possible.
+
The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.
Note that the system option @{system_option_ref jedit_print_mode} allows to
do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close> dialog of
--- a/src/Doc/System/Environment.thy Fri Jun 29 15:22:30 2018 +0100
+++ b/src/Doc/System/Environment.thy Fri Jun 29 22:14:33 2018 +0200
@@ -407,6 +407,7 @@
Options are:
-d DIR include session directory
+ -i NAME include session in name-space of theories
-l NAME logic session name (default ISABELLE_LOGIC)
-m MODE add print mode for output
-n no build of session image on startup
@@ -421,6 +422,9 @@
Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
+ Option \<^verbatim>\<open>-i\<close> includes additional sessions into the name-space of theories:
+ multiple occurrences are possible.
+
Option \<^verbatim>\<open>-r\<close> indicates a bootstrap from the raw Poly/ML system, which is
relevant for Isabelle/Pure development.
--- a/src/FOL/ex/Miniscope.thy Fri Jun 29 15:22:30 2018 +0100
+++ b/src/FOL/ex/Miniscope.thy Fri Jun 29 22:14:33 2018 +0200
@@ -17,14 +17,19 @@
subsubsection \<open>de Morgan laws\<close>
-lemma demorgans:
+lemma demorgans1:
"\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"
"\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q"
"\<not> \<not> P \<longleftrightarrow> P"
+ by blast+
+
+lemma demorgans2:
"\<And>P. \<not> (\<forall>x. P(x)) \<longleftrightarrow> (\<exists>x. \<not> P(x))"
"\<And>P. \<not> (\<exists>x. P(x)) \<longleftrightarrow> (\<forall>x. \<not> P(x))"
by blast+
+lemmas demorgans = demorgans1 demorgans2
+
(*** Removal of --> and <-> (positive and negative occurrences) ***)
(*Last one is important for computing a compact CNF*)
lemma nnf_simps:
--- a/src/HOL/Euclidean_Division.thy Fri Jun 29 15:22:30 2018 +0100
+++ b/src/HOL/Euclidean_Division.thy Fri Jun 29 22:14:33 2018 +0200
@@ -1638,7 +1638,7 @@
by (simp only: *, simp only: l q divide_int_unfold)
(auto simp add: sgn_mult sgn_0_0 sgn_1_pos algebra_simps dest: dvd_imp_le)
qed
-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>)
+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>)
end
--- a/src/HOL/Fields.thy Fri Jun 29 15:22:30 2018 +0100
+++ b/src/HOL/Fields.thy Fri Jun 29 22:14:33 2018 +0200
@@ -843,10 +843,6 @@
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
explosions.\<close>
-lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
-
-lemmas (in -) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
-
(* Only works once linear arithmetic is installed:
text{*An example:*}
lemma fixes a b c d e f :: "'a::linordered_field"
--- a/src/HOL/Metis_Examples/Big_O.thy Fri Jun 29 15:22:30 2018 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy Fri Jun 29 22:14:33 2018 +0200
@@ -457,7 +457,7 @@
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>)"
by (metis mult_left_mono)
then show "\<exists>ca::'a. \<forall>x::'b. inverse \<bar>c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
- using A2 F4 by (metis F1 \<open>0 < \<bar>inverse c\<bar>\<close> linordered_field_class.sign_simps(23) mult_le_cancel_left_pos)
+ using A2 F4 by (metis F1 \<open>0 < \<bar>inverse c\<bar>\<close> mult.assoc mult_le_cancel_left_pos)
qed
lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) <= O(f)"
--- a/src/HOL/Num.thy Fri Jun 29 15:22:30 2018 +0100
+++ b/src/HOL/Num.thy Fri Jun 29 22:14:33 2018 +0200
@@ -1282,14 +1282,20 @@
numeral for 1 reduces the number of special cases.
\<close>
-lemma mult_1s:
+lemma mult_1s_semiring_numeral:
"Numeral1 * a = a"
"a * Numeral1 = a"
+ for a :: "'a::semiring_numeral"
+ by simp_all
+
+lemma mult_1s_ring_1:
"- Numeral1 * b = - b"
"b * - Numeral1 = - b"
- for a :: "'a::semiring_numeral" and b :: "'b::ring_1"
+ for b :: "'a::ring_1"
by simp_all
+lemmas mult_1s = mult_1s_semiring_numeral mult_1s_ring_1
+
setup \<open>
Reorient_Proc.add
(fn Const (@{const_name numeral}, _) $ _ => true
@@ -1385,13 +1391,20 @@
"- numeral v + (- numeral w + y) = (- numeral(v + w) + y)"
by (simp_all add: add.assoc [symmetric])
-lemma mult_numeral_left [simp]:
+lemma mult_numeral_left_semiring_numeral:
"numeral v * (numeral w * z) = (numeral(v * w) * z :: 'a::semiring_numeral)"
- "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
- "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
- "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"
+ by (simp add: mult.assoc [symmetric])
+
+lemma mult_numeral_left_ring_1:
+ "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'a::ring_1)"
+ "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'a::ring_1)"
+ "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'a::ring_1)"
by (simp_all add: mult.assoc [symmetric])
+lemmas mult_numeral_left [simp] =
+ mult_numeral_left_semiring_numeral
+ mult_numeral_left_ring_1
+
hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec
--- a/src/HOL/Rat.thy Fri Jun 29 15:22:30 2018 +0100
+++ b/src/HOL/Rat.thy Fri Jun 29 22:14:33 2018 +0200
@@ -529,6 +529,10 @@
end
+lemmas (in linordered_field) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
+lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
+
+
instantiation rat :: distrib_lattice
begin
--- a/src/Pure/Isar/attrib.ML Fri Jun 29 15:22:30 2018 +0100
+++ b/src/Pure/Isar/attrib.ML Fri Jun 29 22:14:33 2018 +0200
@@ -591,6 +591,7 @@
register_config ML_Options.exception_trace_raw #>
register_config ML_Options.exception_debugger_raw #>
register_config ML_Options.debugger_raw #>
+ register_config Global_Theory.pending_shyps_raw #>
register_config Proof_Context.show_abbrevs_raw #>
register_config Goal_Display.goals_limit_raw #>
register_config Goal_Display.show_main_goal_raw #>
--- a/src/Pure/ML/ml_console.scala Fri Jun 29 15:22:30 2018 +0100
+++ b/src/Pure/ML/ml_console.scala Fri Jun 29 22:14:33 2018 +0200
@@ -15,6 +15,7 @@
{
Command_Line.tool {
var dirs: List[Path] = Nil
+ var include_sessions: List[String] = Nil
var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
var modes: List[String] = Nil
var no_build = false
@@ -27,6 +28,7 @@
Options are:
-d DIR include session directory
+ -i NAME include session in name-space of theories
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
-m MODE add print mode for output
-n no build of session image on startup
@@ -39,6 +41,7 @@
quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
""",
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
"l:" -> (arg => logic = arg),
"m:" -> (arg => modes = arg :: modes),
"n" -> (arg => no_build = true),
@@ -69,7 +72,8 @@
store = Some(Sessions.store(options, system_mode)),
session_base =
if (raw_ml_system) None
- else Some(Sessions.base_info(options, logic, dirs = dirs).check_base))
+ else Some(Sessions.base_info(
+ options, logic, dirs = dirs, include_sessions = include_sessions).check_base))
val tty_loop = new TTY_Loop(process.stdin, process.stdout, Some(process.interrupt _))
val process_result = Future.thread[Int]("process_result") {
--- a/src/Pure/PIDE/document.ML Fri Jun 29 15:22:30 2018 +0100
+++ b/src/Pure/PIDE/document.ML Fri Jun 29 22:14:33 2018 +0200
@@ -735,8 +735,9 @@
segments = segments};
in
fn _ =>
- (Thy_Info.apply_presentation presentation_context thy;
- commit_consolidated node)
+ Exn.release
+ (Exn.capture (Thy_Info.apply_presentation presentation_context) thy
+ before commit_consolidated node)
end
else fn _ => commit_consolidated node;
--- a/src/Pure/Thy/export_theory.ML Fri Jun 29 15:22:30 2018 +0100
+++ b/src/Pure/Thy/export_theory.ML Fri Jun 29 22:14:33 2018 +0200
@@ -102,6 +102,12 @@
(* axioms and facts *)
+ val standard_prop_of =
+ Thm.transfer thy #>
+ Thm.check_hyps (Context.Theory thy) #>
+ Drule.sort_constraint_intr_shyps #>
+ Thm.full_prop_of;
+
val encode_props =
let open XML.Encode Term_XML.Encode
in triple (list (pair string sort)) (list (pair string typ)) (list term) end;
@@ -114,7 +120,7 @@
in encode_props (typargs, args, props') end;
val export_axiom = export_props o single;
- val export_fact = export_props o Term_Subst.zero_var_indexes_list o map Thm.full_prop_of;
+ val export_fact = export_props o Term_Subst.zero_var_indexes_list o map standard_prop_of;
val _ =
export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
--- a/src/Pure/Thy/sessions.scala Fri Jun 29 15:22:30 2018 +0100
+++ b/src/Pure/Thy/sessions.scala Fri Jun 29 22:14:33 2018 +0200
@@ -461,7 +461,11 @@
{
val sel_sessions1 = session1 :: session :: include_sessions
val select_sessions1 =
- if (session_focus) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1
+ if (session_focus) {
+ full_sessions1.check_sessions(sel_sessions1)
+ full_sessions1.imports_descendants(sel_sessions1)
+ }
+ else sel_sessions1
full_sessions1.selection(Selection(sessions = select_sessions1))
}
@@ -679,13 +683,16 @@
}
})
+ def check_sessions(names: List[String])
+ {
+ val bad_sessions = SortedSet(names.filterNot(defined(_)): _*).toList
+ if (bad_sessions.nonEmpty)
+ error("Undefined session(s): " + commas_quote(bad_sessions))
+ }
+
def selection(sel: Selection): Structure =
{
- val bad_sessions =
- SortedSet((sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions).
- filterNot(defined(_)): _*).toList
- if (bad_sessions.nonEmpty)
- error("Undefined session(s): " + commas_quote(bad_sessions))
+ check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
val excluded = sel.excluded(build_graph).toSet
--- a/src/Pure/Tools/dump.scala Fri Jun 29 15:22:30 2018 +0100
+++ b/src/Pure/Tools/dump.scala Fri Jun 29 22:14:33 2018 +0200
@@ -93,8 +93,8 @@
system_mode: Boolean = false,
selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
{
- if (Build.build_logic(options, logic, progress = progress, dirs = dirs,
- system_mode = system_mode) != 0) error(logic + " FAILED")
+ if (Build.build_logic(options, logic, build_heap = true, progress = progress,
+ dirs = dirs, system_mode = system_mode) != 0) error(logic + " FAILED")
val dump_options = make_options(options, aspects)
--- a/src/Pure/drule.ML Fri Jun 29 15:22:30 2018 +0100
+++ b/src/Pure/drule.ML Fri Jun 29 22:14:33 2018 +0200
@@ -98,6 +98,8 @@
val is_sort_constraint: term -> bool
val sort_constraintI: thm
val sort_constraint_eq: thm
+ val sort_constraint_intr: indexname * sort -> thm -> thm
+ val sort_constraint_intr_shyps: thm -> thm
val with_subgoal: int -> (thm -> thm) -> thm -> thm
val comp_no_flatten: thm * int -> int -> thm -> thm
val rename_bvars: (string * string) list -> thm -> thm
@@ -647,6 +649,26 @@
(Thm.unvarify_global (Context.the_global_context ()) sort_constraintI)))
(implies_intr_list [A, C] (Thm.assume A)));
+val sort_constraint_eq' = Thm.symmetric sort_constraint_eq;
+
+fun sort_constraint_intr tvar thm =
+ Thm.equal_elim
+ (Thm.instantiate
+ ([((("'a", 0), []), Thm.global_ctyp_of (Thm.theory_of_thm thm) (TVar tvar))],
+ [((("A", 0), propT), Thm.cprop_of thm)])
+ sort_constraint_eq') thm;
+
+fun sort_constraint_intr_shyps raw_thm =
+ let val thm = Thm.strip_shyps raw_thm in
+ (case Thm.extra_shyps thm of
+ [] => thm
+ | shyps =>
+ let
+ val names = Name.make_context (map #1 (Thm.fold_terms Term.add_tvar_names thm []));
+ val constraints = map (rpair 0) (Name.invent names Name.aT (length shyps)) ~~ shyps;
+ in Thm.strip_shyps (fold_rev sort_constraint_intr constraints thm) end)
+ end;
+
end;
--- a/src/Pure/global_theory.ML Fri Jun 29 15:22:30 2018 +0100
+++ b/src/Pure/global_theory.ML Fri Jun 29 22:14:33 2018 +0200
@@ -24,6 +24,8 @@
val name_thm: bool -> bool -> string -> thm -> thm
val name_thms: bool -> bool -> string -> thm list -> thm list
val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
+ val pending_shyps_raw: Config.raw
+ val pending_shyps: bool Config.T
val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
val store_thm: binding * thm -> theory -> thm * theory
val store_thm_open: binding * thm -> theory -> thm * theory
@@ -128,16 +130,35 @@
fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
+val pending_shyps_raw = Config.declare ("pending_shyps", \<^here>) (K (Config.Bool false));
+val pending_shyps = Config.bool pending_shyps_raw;
+
fun add_facts (b, fact) thy =
let
val full_name = Sign.full_name thy b;
val pos = Binding.pos_of b;
- fun err msg =
- error ("Malformed global fact " ^ quote full_name ^ Position.here pos ^ "\n" ^ msg);
- fun check thm =
- ignore (Logic.unvarify_global (Term_Subst.zero_var_indexes (Thm.full_prop_of thm)))
- handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
- val arg = (b, Lazy.map_finished (tap (List.app check)) fact);
+ fun check fact =
+ fact |> map_index (fn (i, thm) =>
+ let
+ fun err msg =
+ error ("Malformed global fact " ^
+ quote (full_name ^
+ (if length fact = 1 then "" else "(" ^ string_of_int (i + 1) ^ ")")) ^
+ Position.here pos ^ "\n" ^ msg);
+ val prop = Thm.plain_prop_of thm
+ handle THM _ =>
+ thm
+ |> not (Config.get_global thy pending_shyps) ?
+ Thm.check_shyps (Proof_Context.init_global thy)
+ |> Thm.check_hyps (Context.Theory thy)
+ |> Thm.full_prop_of;
+ in
+ ignore (Logic.unvarify_global (Term_Subst.zero_var_indexes prop))
+ handle TYPE (msg, _, _) => err msg
+ | TERM (msg, _) => err msg
+ | ERROR msg => err msg
+ end);
+ val arg = (b, Lazy.map_finished (tap check) fact);
in
thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
end;
--- a/src/Tools/VSCode/extension/README.md Fri Jun 29 15:22:30 2018 +0100
+++ b/src/Tools/VSCode/extension/README.md Fri Jun 29 22:14:33 2018 +0200
@@ -1,14 +1,15 @@
# Isabelle Prover IDE support
This extension connects VSCode to the Isabelle Prover IDE infrastructure: it
-requires a repository version of Isabelle.
+requires Isabelle2018.
The implementation is centered around the VSCode Language Server protocol, but
with many add-ons that are specific to VSCode and Isabelle/PIDE.
See also:
- * <https://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode>
+ * <https://isabelle.in.tum.de/website-Isabelle2018>
+ * <https://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/Tools/VSCode>
* <https://github.com/Microsoft/language-server-protocol>
@@ -58,8 +59,8 @@
### Isabelle/VSCode Installation
- * Download a recent Isabelle development snapshot from
- <http://isabelle.in.tum.de/devel/release_snapshot>
+ * Download Isabelle2018 from <https://isabelle.in.tum.de/website-Isabelle2018>
+ or any of its mirror sites.
* Unpack and run the main Isabelle/jEdit application as usual, to ensure that
the logic image is built properly and Isabelle works as expected.
@@ -68,7 +69,7 @@
* Open the VSCode *Extensions* view and install the following:
- + *Isabelle*.
+ + *Isabelle2018* (needs to fit to the underlying Isabelle release).
+ *Prettify Symbols Mode* (important for display of Isabelle symbols).
@@ -89,17 +90,17 @@
+ Linux:
```
- "isabelle.home": "/home/makarius/Isabelle"
+ "isabelle.home": "/home/makarius/Isabelle2018"
```
+ Mac OS X:
```
- "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle"
+ "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle2018"
```
+ Windows:
```
- "isabelle.home": "C:\\Users\\makarius\\Isabelle"
+ "isabelle.home": "C:\\Users\\makarius\\Isabelle2018"
```
* Restart the VSCode application to ensure that all extensions are properly
--- a/src/Tools/VSCode/extension/package.json Fri Jun 29 15:22:30 2018 +0100
+++ b/src/Tools/VSCode/extension/package.json Fri Jun 29 22:14:33 2018 +0200
@@ -1,6 +1,6 @@
{
- "name": "isabelle",
- "displayName": "Isabelle",
+ "name": "Isabelle2018",
+ "displayName": "Isabelle2018",
"description": "Isabelle Prover IDE",
"keywords": [
"theorem prover",
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Jun 29 15:22:30 2018 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Fri Jun 29 22:14:33 2018 +0200
@@ -106,6 +106,7 @@
echo " -b build only"
echo " -d DIR include session directory"
echo " -f fresh build"
+ echo " -i NAME include session in name-space of theories"
echo " -j OPTION add jEdit runtime option"
echo " (default $JEDIT_OPTIONS)"
echo " -l NAME logic session name"
@@ -142,6 +143,7 @@
JEDIT_LOGIC_ANCESTOR=""
JEDIT_LOGIC_REQUIREMENTS=""
JEDIT_LOGIC_FOCUS=""
+JEDIT_INCLUDE_SESSIONS=""
JEDIT_SESSION_DIRS=""
JEDIT_LOGIC=""
JEDIT_PRINT_MODE=""
@@ -150,7 +152,7 @@
function getoptions()
{
OPTIND=1
- while getopts "A:BFD:J:R:S:bd:fj:l:m:np:s" OPT
+ while getopts "A:BFD:J:R:S:bd:fi:j:l:m:np:s" OPT
do
case "$OPT" in
A)
@@ -181,6 +183,13 @@
JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
fi
;;
+ i)
+ if [ -z "$JEDIT_INCLUDE_SESSIONS" ]; then
+ JEDIT_INCLUDE_SESSIONS="$OPTARG"
+ else
+ JEDIT_INCLUDE_SESSIONS="$JEDIT_INCLUDE_SESSIONS:$OPTARG"
+ fi
+ ;;
f)
BUILD_JARS="jars_fresh"
;;
@@ -413,7 +422,7 @@
if [ "$BUILD_ONLY" = false ]
then
export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
- JEDIT_LOGIC_FOCUS JEDIT_PRINT_MODE JEDIT_BUILD_MODE
+ JEDIT_LOGIC_FOCUS JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_BUILD_MODE
export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
classpath "$JEDIT_HOME/dist/jedit.jar"
exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
--- a/src/Tools/jEdit/src/jedit_sessions.scala Fri Jun 29 15:22:30 2018 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Jun 29 22:14:33 2018 +0200
@@ -42,6 +42,8 @@
def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR"))
def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true"
def logic_focus: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_FOCUS") == "true"
+ def logic_include_sessions: List[String] =
+ space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS"))
def logic_info(options: Options): Option[Sessions.Info] =
try {
@@ -108,6 +110,7 @@
def session_base_info(options: Options): Sessions.Base_Info =
Sessions.base_info(options,
dirs = JEdit_Sessions.session_dirs(),
+ include_sessions = logic_include_sessions,
session = logic_name(options),
session_ancestor = logic_ancestor,
session_requirements = logic_requirements,