--- a/ANNOUNCE Wed Jun 06 14:25:53 2018 +0100
+++ b/ANNOUNCE Wed Jun 06 14:27:10 2018 +0100
@@ -1,32 +1,15 @@
-Subject: Announcing Isabelle2017
+Subject: Announcing Isabelle2018
To: isabelle-users@cl.cam.ac.uk
-Isabelle2017 is now available.
+Isabelle2018 is now available.
-This version introduces many changes over Isabelle2016-1: see the NEWS
+This version introduces many changes over Isabelle2017: see the NEWS
file for further details. Some notable points:
-* Experimental support for Visual Studio Code as alternative PIDE front-end.
-
-* Improved Isabelle/jEdit Prover IDE: management of session sources
-independently of editor buffers, removal of unused theories, explicit
-indication of theory status, more careful auto-indentation.
-
-* Session-qualified theory imports.
-
-* Code generator improvements: support for statically embedded computations.
-
-* Numerous HOL library improvements.
-
-* More material in HOL-Algebra, HOL-Computational_Algebra and HOL-Analysis
-(ported from HOL-Light).
-
-* Improved Nunchaku model finder, now in main HOL.
-
-* SQL database support in Isabelle/Scala.
+* FIXME.
-You may get Isabelle2017 from the following mirror sites:
+You may get Isabelle2018 from the following mirror sites:
Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle
Munich (Germany) http://isabelle.in.tum.de
--- a/Admin/components/components.sha1 Wed Jun 06 14:25:53 2018 +0100
+++ b/Admin/components/components.sha1 Wed Jun 06 14:27:10 2018 +0100
@@ -215,6 +215,7 @@
b016a785f1f78855c00d351ff598355c3b87450f sqlite-jdbc-3.18.0-1.tar.gz
b85b5bc071a59ef2a8326ceb1617d5a9a5be41cf sqlite-jdbc-3.18.0.tar.gz
e56117a67ab01fb24c7fc054ede3160cefdac5f8 sqlite-jdbc-3.20.0.tar.gz
+27aeac6a91353d69f0438837798ac4ae6f9ff8c5 sqlite-jdbc-3.23.1.tar.gz
8d20968603f45a2c640081df1ace6a8b0527452a sqlite-jdbc-3.8.11.2.tar.gz
2369f06e8d095f9ba26df938b1a96000e535afff ssh-java-20161009.tar.gz
1f4a2053cc1f34fa36c4d9d2ac906ad4ebc863fd sumatra_pdf-2.1.1.tar.gz
--- a/Admin/components/main Wed Jun 06 14:25:53 2018 +0100
+++ b/Admin/components/main Wed Jun 06 14:27:10 2018 +0100
@@ -17,7 +17,7 @@
smbc-0.4.1
ssh-java-20161009
spass-3.8ds-1
-sqlite-jdbc-3.20.0
+sqlite-jdbc-3.23.1
verit-2016post
xz-java-1.8
z3-4.4.0pre-2
--- a/CONTRIBUTORS Wed Jun 06 14:25:53 2018 +0100
+++ b/CONTRIBUTORS Wed Jun 06 14:27:10 2018 +0100
@@ -3,11 +3,11 @@
listed as an author in one of the source files of this Isabelle distribution.
-Contributions to this Isabelle version
---------------------------------------
+Contributions to Isabelle2018
+-----------------------------
* May 2018: Manuel Eberl
- Landau symbols and asymptotic equivalence (moved from the AFP)
+ Landau symbols and asymptotic equivalence (moved from the AFP).
* May 2018: Jose Divasón (Universidad de la Rioja),
Jesús Aransay (Universidad de la Rioja), Johannes Hölzl (VU Amsterdam),
@@ -22,9 +22,8 @@
Code generation with lazy evaluation semantics.
* March 2018: Florian Haftmann
- Abstract bit operations push_bit, take_bit, drop_bit, alongside
- with an algebraic foundation for bit strings and word types in
- HOL-ex.
+ Abstract bit operations push_bit, take_bit, drop_bit, alongside with an
+ algebraic foundation for bit strings and word types in HOL-ex.
* March 2018: Viorel Preoteasa
Generalisation of complete_distrib_lattice
@@ -36,7 +35,8 @@
A new conditional parametricity prover.
* October 2017: Alexander Maletzky
- Derivation of axiom "iff" in HOL.thy from the other axioms.
+ Derivation of axiom "iff" in theory HOL.HOL from the other axioms.
+
Contributions to Isabelle2017
-----------------------------
--- a/COPYRIGHT Wed Jun 06 14:25:53 2018 +0100
+++ b/COPYRIGHT Wed Jun 06 14:27:10 2018 +0100
@@ -1,6 +1,6 @@
ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.
-Copyright (c) 1986-2017,
+Copyright (c) 1986-2018,
University of Cambridge,
Technische Universitaet Muenchen,
and contributors.
--- a/NEWS Wed Jun 06 14:25:53 2018 +0100
+++ b/NEWS Wed Jun 06 14:27:10 2018 +0100
@@ -4,11 +4,21 @@
(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
-New in this Isabelle version
-----------------------------
+New in Isabelle2018 (August 2018)
+---------------------------------
*** General ***
+* Session-qualified theory names are mandatory: it is no longer possible
+to refer to unqualified theories from the parent session.
+INCOMPATIBILITY for old developments that have not been updated to
+Isabelle2017 yet (using the "isabelle imports" tool).
+
+* Only the most fundamental theory names are global, usually the entry
+points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
+FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
+formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
+
* 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
@@ -29,23 +39,9 @@
In case you want to exclude conversion of ML files (because the tool
frequently also converts ML's "op" syntax), use option "-m".
-* The old 'def' command has been discontinued (legacy since
-Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
-object-logic equality or equivalence.
-
-* Session-qualified theory names are mandatory: it is no longer possible
-to refer to unqualified theories from the parent session.
-INCOMPATIBILITY for old developments that have not been updated to
-Isabelle2017 yet (using the "isabelle imports" tool).
-
* Theory header 'abbrevs' specifications need to be separated by 'and'.
INCOMPATIBILITY.
-* Only the most fundamental theory names are global, usually the entry
-points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
-FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
-formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
-
* Command 'external_file' declares the formal dependency on the given
file name, such that the Isabelle build process knows about it, but
without specific Prover IDE management.
@@ -64,13 +60,45 @@
* The command 'display_drafts' has been discontinued. INCOMPATIBILITY,
use action "isabelle.draft" (or "print") in Isabelle/jEdit instead.
-* Isabelle symbol "\<hyphen>" is rendered as explicit Unicode hyphen U+2010, to
-avoid unclear meaning of the old "soft hyphen" U+00AD. Rare
-INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML output.
+* In HTML output, the Isabelle symbol "\<hyphen>" is rendered as explicit
+Unicode hyphen U+2010, to avoid unclear meaning of the old "soft hyphen"
+U+00AD. Rare INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML
+output.
*** Isabelle/jEdit Prover IDE ***
+* The command-line tool "isabelle jedit" provides more flexible options
+for session management:
+
+ - option -R builds an auxiliary logic image with all required theories
+ from other sessions, relative to an ancestor session given by option
+ -A (default: parent)
+
+ - option -S is like -R, with a focus on the selected session and its
+ descendants (this reduces startup time for big projects like AFP)
+
+ 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
+
+* PIDE markup for session ROOT files: allows to complete session names,
+follow links to theories and document files etc.
+
+* Completion supports theory header imports, using theory base name.
+E.g. "Prob" may be completed to "HOL-Probability.Probability".
+
+* Named control symbols (without special Unicode rendering) are shown as
+bold-italic keyword. This is particularly useful for the short form of
+antiquotations with control symbol: \<^name>\<open>argument\<close>. The action
+"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
+arguments into this format.
+
+* Completion provides templates for named symbols with arguments,
+e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".
+
* Slightly more parallel checking, notably for high priority print
functions (e.g. State output).
@@ -82,37 +110,6 @@
supersede former "spell_checker_elements" to determine regions of text
that are subject to spell-checking. Minor INCOMPATIBILITY.
-* PIDE markup for session ROOT files: allows to complete session names,
-follow links to theories and document files etc.
-
-* Completion supports theory header imports, using theory base name.
-E.g. "Prob" may be completed to "HOL-Probability.Probability".
-
-* The command-line tool "isabelle jedit" provides more flexible options
-for session management:
- - option -R builds an auxiliary logic image with all required theories
- from other sessions, relative to an ancestor session given by option
- -A (default: parent)
- - option -S is like -R, with a focus on the selected session and its
- descendants (this reduces startup time for big projects like AFP)
-
- 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
-
-* Named control symbols (without special Unicode rendering) are shown as
-bold-italic keyword. This is particularly useful for the short form of
-antiquotations with control symbol: \<^name>\<open>argument\<close>. The action
-"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
-arguments into this format.
-
-* Completion provides templates for named symbols with arguments,
-e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".
-
-* Bibtex database files (.bib) are semantically checked.
-
* Action "isabelle.preview" is able to present more file formats,
notably bibtex database files and ML files.
@@ -120,6 +117,8 @@
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
@@ -163,19 +162,23 @@
antiquotations in control symbol notation, e.g. \<^const_name> becomes
\isactrlconstUNDERSCOREname.
-* Document antiquotation @{cite} now checks the given Bibtex entries
-against the Bibtex database files -- only in batch-mode session builds.
+* Document preparation with skip_proofs option now preserves the content
+more accurately: only terminal proof steps ('by' etc.) are skipped.
* Document antiquotation @{session name} checks and prints the given
session name verbatim.
-* Document preparation with skip_proofs option now preserves the content
-more accurately: only terminal proof steps ('by' etc.) are skipped.
+* Document antiquotation @{cite} now checks the given Bibtex entries
+against the Bibtex database files -- only in batch-mode session builds.
* Command-line tool "isabelle document" has been re-implemented in
Isabelle/Scala, with simplified arguments and explicit errors from the
latex and bibtex process. Minor INCOMPATIBILITY.
+* Session ROOT entry: empty 'document_files' means there is no document
+for this session. There is no need to specify options [document = false]
+anymore.
+
*** Isar ***
@@ -185,13 +188,17 @@
Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
(e.g. use 'find_theorems' or 'try' to figure this out).
+* The old 'def' command has been discontinued (legacy since
+Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
+object-logic equality or equivalence.
+
* 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' and 'defines'. Minor INCOMPATIBILITY.
-
-* For rewrites clauses, if activating a locale instance fails, fall
-back to reading the clause first. This helps avoid qualification of
+expression syntax, where they are part of locale instances. In
+interpretation commands rewrites clauses now need to occur before 'for'
+and 'defines'. Minor INCOMPATIBILITY.
+
+* For 'rewrites' clauses, if activating a locale instance fails, fall
+back to reading the clause first. This helps avoid qualification of
locale instances where the qualifier's sole purpose is avoiding
duplicate constant declarations.
@@ -204,54 +211,55 @@
*** HOL ***
-* Landau_Symbols from the AFP was moved to HOL-Library
-
* Clarified relationship of characters, strings and code generation:
- * Type "char" is now a proper datatype of 8-bit values.
-
- * Conversions "nat_of_char" and "char_of_nat" are gone; use more
- general conversions "of_char" and "char_of" with suitable
- type constraints instead.
-
- * The zero character is just written "CHR 0x00", not
- "0" any longer.
-
- * Type "String.literal" (for code generation) is now isomorphic
- to lists of 7-bit (ASCII) values; concrete values can be written
- as "STR ''...''" for sequences of printable characters and
- "STR 0x..." for one single ASCII code point given
- as hexadecimal numeral.
-
- * Type "String.literal" supports concatenation "... + ..."
- for all standard target languages.
-
- * Theory Library/Code_Char is gone; study the explanations concerning
- "String.literal" in the tutorial on code generation to get an idea
- how target-language string literals can be converted to HOL string
- values and vice versa.
-
- * Imperative-HOL: operation "raise" directly takes a value of type
- "String.literal" as argument, not type "string".
-
-INCOMPATIBILITY.
-
-* Abstract bit operations as part of Main: push_bit, take_bit,
-drop_bit.
-
-* New, more general, axiomatization of complete_distrib_lattice.
-The former axioms:
-"sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
-are replaced by
-"Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
-The instantiations of sets and functions as complete_distrib_lattice
-are moved to Hilbert_Choice.thy because their proofs need the Hilbert
-choice operator. The dual of this property is also proved in
-Hilbert_Choice.thy.
+ - Type "char" is now a proper datatype of 8-bit values.
+
+ - Conversions "nat_of_char" and "char_of_nat" are gone; use more
+ general conversions "of_char" and "char_of" with suitable type
+ constraints instead.
+
+ - The zero character is just written "CHR 0x00", not "0" any longer.
+
+ - Type "String.literal" (for code generation) is now isomorphic to
+ lists of 7-bit (ASCII) values; concrete values can be written as
+ "STR ''...''" for sequences of printable characters and "STR 0x..."
+ for one single ASCII code point given as hexadecimal numeral.
+
+ - Type "String.literal" supports concatenation "... + ..." for all
+ standard target languages.
+
+ - Theory HOL-Library.Code_Char is gone; study the explanations
+ concerning "String.literal" in the tutorial on code generation to
+ get an idea how target-language string literals can be converted to
+ HOL string values and vice versa.
+
+ - Session Imperative-HOL: operation "raise" directly takes a value of
+ type "String.literal" as argument, not type "string".
+
+INCOMPATIBILITY.
+
+* Code generation: Code generation takes an explicit option
+"case_insensitive" to accomodate case-insensitive file systems.
+
+* Abstract bit operations as part of Main: push_bit, take_bit, drop_bit.
+
+* New, more general, axiomatization of complete_distrib_lattice. The
+former axioms:
+
+ "sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
+
+are replaced by:
+
+ "Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
+
+The instantiations of sets and functions as complete_distrib_lattice are
+moved to Hilbert_Choice.thy because their proofs need the Hilbert choice
+operator. The dual of this property is also proved in theory
+HOL.Hilbert_Choice.
* New syntax for the minimum/maximum of a function over a finite set:
-MIN x\<in>A. B and even MIN x. B (only useful for finite types), also
-MAX.
+MIN x\<in>A. B and even MIN x. B (only useful for finite types), also MAX.
* Clarifed theorem names:
@@ -260,83 +268,59 @@
Minor INCOMPATIBILITY.
-* A new command parametric_constant for proving parametricity of
-non-recursive definitions. For constants that are not fully parametric
-the command will infer conditions on relations (e.g., bi_unique,
-bi_total, or type class conditions such as "respects 0") sufficient for
-parametricity. See ~~/src/HOL/ex/Conditional_Parametricity_Examples for
-some examples.
-
-* A new preprocessor for the code generator to generate code for algebraic
- types with lazy evaluation semantics even in call-by-value target languages.
- See theory HOL-Library.Code_Lazy for the implementation and
- HOL-Codegenerator_Test.Code_Lazy_Test for examples.
-
* SMT module:
+
- The 'smt_oracle' option is now necessary when using the 'smt' method
with a solver other than Z3. INCOMPATIBILITY.
+
- The encoding to first-order logic is now more complete in the
presence of higher-order quantifiers. An 'smt_explicit_application'
option has been added to control this. INCOMPATIBILITY.
-* Datatypes:
- - The legacy command 'old_datatype', provided by
- '~~/src/HOL/Library/Old_Datatype.thy', has been removed. INCOMPATIBILITY.
-
-* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide
-instances of rat, real, complex as factorial rings etc. Import
-HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
-INCOMPATIBILITY.
-
* Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to
sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on
interpretation of abstract locales. INCOMPATIBILITY.
+* Predicate coprime is now a real definition, not a mere abbreviation.
+INCOMPATIBILITY.
+
* Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
INCOMPATIBILITY.
* The relator rel_filter on filters has been strengthened to its
-canonical categorical definition with better properties. INCOMPATIBILITY.
+canonical categorical definition with better properties.
+INCOMPATIBILITY.
* Generalized linear algebra involving linear, span, dependent, dim
from type class real_vector to locales module and vector_space.
Renamed:
- - span_inc ~> span_superset
- - span_superset ~> span_base
- - span_eq ~> span_eq_iff
-INCOMPATIBILITY.
-
-* HOL-Algebra: renamed (^) to [^]
-
-* Session HOL-Analysis: infinite products, Moebius functions, the Riemann mapping
-theorem, the Vitali covering theorem, change-of-variables results for
-integration and measures.
+
+ span_inc ~> span_superset
+ span_superset ~> span_base
+ span_eq ~> span_eq_iff
+
+INCOMPATIBILITY.
* Class linordered_semiring_1 covers zero_less_one also, ruling out
pathologic instances. Minor INCOMPATIBILITY.
-* Theory List: functions "sorted_wrt" and "sorted" now compare every
- element in a list to all following elements, not just the next one.
-
-* Theory List: Synatx:
- - filter-syntax "[x <- xs. P]" is no longer output syntax
- but only input syntax.
- - list comprehension syntax now supports tuple patterns in "pat <- xs".
+* Theory HOL.List: functions "sorted_wrt" and "sorted" now compare every
+element in a list to all following elements, not just the next one.
+
+* Theory HOL.List syntax:
+
+ - filter-syntax "[x <- xs. P]" is no longer output syntax, but only
+ input syntax
+
+ - list comprehension syntax now supports tuple patterns in "pat <- xs"
* Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
-* Predicate coprime is now a real definition, not a mere
-abbreviation. INCOMPATIBILITY.
-
-* Code generation: Code generation takes an explicit option
-"case_insensitive" to accomodate case-insensitive file systems.
-
* Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid
clash with fact mod_mult_self4 (on more generic semirings).
INCOMPATIBILITY.
* Eliminated some theorem aliasses:
-
even_times_iff ~> even_mult_iff
mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1
even_of_nat ~> even_int_iff
@@ -344,18 +328,48 @@
INCOMPATIBILITY.
* Eliminated some theorem duplicate variations:
- * dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0.
- * mod_Suc_eq_Suc_mod can be replaced by mod_Suc.
- * mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps.
- * mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def.
- * The witness of mod_eqD can be given directly as "_ div _".
+
+ - dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0
+ - mod_Suc_eq_Suc_mod can be replaced by mod_Suc
+ - mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps
+ - mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def
+ - the witness of mod_eqD can be given directly as "_ div _"
INCOMPATIBILITY.
* Classical setup: Assumption "m mod d = 0" (for m d :: nat) is no
-longer aggresively destroyed to "?q. m = d * q". INCOMPATIBILITY,
-adding "elim!: dvd" to classical proof methods in most situations
-restores broken proofs.
+longer aggresively destroyed to "\<exists>q. m = d * q". INCOMPATIBILITY, adding
+"elim!: dvd" to classical proof methods in most situations restores
+broken proofs.
+
+* Theory HOL-Library.Conditional_Parametricity provides command
+'parametric_constant' for proving parametricity of non-recursive
+definitions. For constants that are not fully parametric the command
+will infer conditions on relations (e.g., bi_unique, bi_total, or type
+class conditions such as "respects 0") sufficient for parametricity. See
+theory HOL-ex.Conditional_Parametricity_Examples for some examples.
+
+* Theory HOL-Library.Code_Lazy provides a new preprocessor for the code
+generator to generate code for algebraic types with lazy evaluation
+semantics even in call-by-value target languages. See theory
+HOL-Codegenerator_Test.Code_Lazy_Test for some examples.
+
+* Theory HOL-Library.Landau_Symbols has been moved here from AFP.
+
+* Theory HOL-Library.Old_Datatype no longer provides the legacy command
+'old_datatype'. INCOMPATIBILITY.
+
+* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide
+instances of rat, real, complex as factorial rings etc. Import
+HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
+INCOMPATIBILITY.
+
+* Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new
+infix/prefix notation.
+
+* Session HOL-Analysis: infinite products, Moebius functions, the
+Riemann mapping theorem, the Vitali covering theorem,
+change-of-variables results for integration and measures.
*** ML ***
@@ -371,47 +385,12 @@
*** System ***
-* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:
-heap images and session databases are always stored in
-$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER (command-line default) or
-$ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or
-"isabelle jedit -s" or "isabelle build -s").
-
-* The command-line tool "export" and 'export_files' in session ROOT
-entries retrieve theory exports from the session build database.
-
-* The command-line tools "isabelle server" and "isabelle client" provide
-access to the Isabelle Server: it supports responsive session management
-and concurrent use of theories, based on Isabelle/PIDE infrastructure.
-See also the "system" manual.
-
-* The command-line tool "dump" dumps information from the cumulative
-PIDE session database: many sessions may be loaded into a given logic
-image, results from all loaded theories are written to the output
-directory.
-
-* The command-line tool "isabelle update_comments" normalizes formal
-comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
-approximate the appearance in document output). This is more specific
-than former "isabelle update_cartouches -c": the latter tool option has
-been discontinued.
-
-* Session ROOT entry: empty 'document_files' means there is no document
-for this session. There is no need to specify options [document = false]
-anymore.
-
-* The command-line tool "isabelle mkroot" now always produces a document
-outline: its options have been adapted accordingly. INCOMPATIBILITY.
-
-* The command-line tool "isabelle mkroot -I" initializes a Mercurial
-repository for the generated session files.
-
-* Linux and Windows/Cygwin is for x86_64 only. Old 32bit platform
-support has been discontinued.
-
* Mac OS X 10.10 Yosemite is now the baseline version; Mavericks is no
longer supported.
+* Linux and Windows/Cygwin is for x86_64 only, old 32bit platform
+support has been discontinued.
+
* Java runtime is for x86_64 only. Corresponding Isabelle settings have
been renamed to ISABELLE_TOOL_JAVA_OPTIONS and JEDIT_JAVA_OPTIONS,
instead of former 32/64 variants. INCOMPATIBILITY.
@@ -439,17 +418,46 @@
corresponding environment values into account, when determining the
up-to-date status of a session.
+* The command-line tool "dump" dumps information from the cumulative
+PIDE session database: many sessions may be loaded into a given logic
+image, results from all loaded theories are written to the output
+directory.
+
* Command-line tool "isabelle imports -I" also reports actual session
imports. This helps to minimize the session dependency graph.
-* Update to current Poly/ML 5.7.1 with slightly improved performance and
-PIDE markup for identifier bindings.
+* The command-line tool "export" and 'export_files' in session ROOT
+entries retrieve theory exports from the session build database.
+
+* The command-line tools "isabelle server" and "isabelle client" provide
+access to the Isabelle Server: it supports responsive session management
+and concurrent use of theories, based on Isabelle/PIDE infrastructure.
+See also the "system" manual.
+
+* The command-line tool "isabelle update_comments" normalizes formal
+comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
+approximate the appearance in document output). This is more specific
+than former "isabelle update_cartouches -c": the latter tool option has
+been discontinued.
+
+* The command-line tool "isabelle mkroot" now always produces a document
+outline: its options have been adapted accordingly. INCOMPATIBILITY.
+
+* The command-line tool "isabelle mkroot -I" initializes a Mercurial
+repository for the generated session files.
+
+* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:
+heap images and session databases are always stored in
+$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER (command-line default) or
+$ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or
+"isabelle jedit -s" or "isabelle build -s").
* ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific
options for improved error reporting. Potential INCOMPATIBILITY with
unusual LaTeX installations, may have to adapt these settings.
-* The bundled Poly/ML 5.7.1 now uses The GNU Multiple Precision
+* Update to Poly/ML 5.7.1 with slightly improved performance and PIDE
+markup for identifier bindings. It now uses The GNU Multiple Precision
Arithmetic Library (libgmp) on all platforms, notably Mac OS X with
32/64 bit.
--- a/etc/settings Wed Jun 06 14:25:53 2018 +0100
+++ b/etc/settings Wed Jun 06 14:27:10 2018 +0100
@@ -134,5 +134,8 @@
ISABELLE_GNUPLOT="gnuplot"
#ISABELLE_GHC="/usr/bin/ghc"
+#ISABELLE_MLTON="/usr/bin/mlton"
#ISABELLE_OCAML="/usr/bin/ocaml"
+#ISABELLE_OCAMLC="/usr/bin/ocamlc"
+#ISABELLE_SMLNJ="/usr/bin/sml"
#ISABELLE_SWIPL="/usr/bin/swipl"
--- a/src/Doc/JEdit/JEdit.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/Doc/JEdit/JEdit.thy Wed Jun 06 14:27:10 2018 +0100
@@ -305,7 +305,7 @@
The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
different server name. The default server name is the official distribution
- name (e.g.\ \<^verbatim>\<open>Isabelle2017\<close>). Thus @{tool jedit_client} can connect to the
+ name (e.g.\ \<^verbatim>\<open>Isabelle2018\<close>). Thus @{tool jedit_client} can connect to the
Isabelle desktop application without further options.
The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
--- a/src/Doc/System/Environment.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/Doc/System/Environment.thy Wed Jun 06 14:27:10 2018 +0100
@@ -58,7 +58,7 @@
\<^enum> The file @{path "$ISABELLE_HOME_USER/etc/settings"} (if it
exists) is run in the same way as the site default settings. Note that the
variable @{setting ISABELLE_HOME_USER} has already been set before ---
- usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2017\<close>.
+ usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2018\<close>.
Thus individual users may override the site-wide defaults. Typically, a
user settings file contains only a few lines, with some assignments that
@@ -149,7 +149,7 @@
of the @{executable isabelle} executable.
\<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
- Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2017\<close>''.
+ Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2018\<close>''.
\<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
--- a/src/Doc/System/Misc.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/Doc/System/Misc.thy Wed Jun 06 14:27:10 2018 +0100
@@ -220,7 +220,7 @@
\<^medskip>
The default is to output the full version string of the Isabelle
- distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2017: October 2017\<close>.
+ distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2018: August 2018\<close>.
The \<^verbatim>\<open>-i\<close> option produces a short identification derived from the Mercurial
id of the @{setting ISABELLE_HOME} directory.
--- a/src/Doc/Tutorial/Inductive/AB.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/Doc/Tutorial/Inductive/AB.thy Wed Jun 06 14:27:10 2018 +0100
@@ -64,13 +64,15 @@
\<close>
lemma correctness:
- "(w \<in> S \<longrightarrow> size(filter (\<lambda>x. x=a) w) = size(filter (\<lambda>x. x=b) w)) \<and>
- (w \<in> A \<longrightarrow> size(filter (\<lambda>x. x=a) w) = size(filter (\<lambda>x. x=b) w) + 1) \<and>
- (w \<in> B \<longrightarrow> size(filter (\<lambda>x. x=b) w) = size(filter (\<lambda>x. x=a) w) + 1)"
+ "(w \<in> S \<longrightarrow> size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b]) \<and>
+ (w \<in> A \<longrightarrow> size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b] + 1) \<and>
+ (w \<in> B \<longrightarrow> size[x\<leftarrow>w. x=b] = size[x\<leftarrow>w. x=a] + 1)"
txt\<open>\noindent
These propositions are expressed with the help of the predefined @{term
-filter} function on lists. Remember that on lists @{text size} and @{text length} are synonymous.
+filter} function on lists, which has the convenient syntax @{text"[x\<leftarrow>xs. P
+x]"}, the list of all elements @{term x} in @{term xs} such that @{prop"P x"}
+holds. Remember that on lists @{text size} and @{text length} are synonymous.
The proof itself is by rule induction and afterwards automatic:
\<close>
@@ -110,8 +112,8 @@
\<close>
lemma step1: "\<forall>i < size w.
- \<bar>(int(size(filter P (take (i+1) w)))-int(size(filter (\<lambda>x. \<not>P x) (take (i+1) w))))
- - (int(size(filter P (take i w)))-int(size(filter (\<lambda>x. \<not>P x) (take i w))))\<bar> \<le> 1"
+ \<bar>(int(size[x\<leftarrow>take (i+1) w. P x])-int(size[x\<leftarrow>take (i+1) w. \<not>P x]))
+ - (int(size[x\<leftarrow>take i w. P x])-int(size[x\<leftarrow>take i w. \<not>P x]))\<bar> \<le> 1"
txt\<open>\noindent
The lemma is a bit hard to read because of the coercion function
@@ -135,8 +137,8 @@
\<close>
lemma part1:
- "size(filter P w) = size(filter (\<lambda>x. \<not>P x) w)+2 \<Longrightarrow>
- \<exists>i\<le>size w. size(filter P (take i w)) = size(filter (\<lambda>x. \<not>P x) (take i w))+1"
+ "size[x\<leftarrow>w. P x] = size[x\<leftarrow>w. \<not>P x]+2 \<Longrightarrow>
+ \<exists>i\<le>size w. size[x\<leftarrow>take i w. P x] = size[x\<leftarrow>take i w. \<not>P x]+1"
txt\<open>\noindent
This is proved by @{text force} with the help of the intermediate value theorem,
@@ -155,10 +157,10 @@
lemma part2:
- "\<lbrakk>size(filter P (take i w @ drop i w)) =
- size(filter (\<lambda>x. \<not>P x) (take i w @ drop i w))+2;
- size(filter P (take i w)) = size(filter (\<lambda>x. \<not>P x) (take i w))+1\<rbrakk>
- \<Longrightarrow> size(filter P (drop i w)) = size(filter (\<lambda>x. \<not>P x) (drop i w))+1"
+ "\<lbrakk>size[x\<leftarrow>take i w @ drop i w. P x] =
+ size[x\<leftarrow>take i w @ drop i w. \<not>P x]+2;
+ size[x\<leftarrow>take i w. P x] = size[x\<leftarrow>take i w. \<not>P x]+1\<rbrakk>
+ \<Longrightarrow> size[x\<leftarrow>drop i w. P x] = size[x\<leftarrow>drop i w. \<not>P x]+1"
by(simp del: append_take_drop_id)
text\<open>\noindent
@@ -185,9 +187,9 @@
\<close>
theorem completeness:
- "(size(filter (\<lambda>x. x=a) w) = size(filter (\<lambda>x. x=b) w) \<longrightarrow> w \<in> S) \<and>
- (size(filter (\<lambda>x. x=a) w) = size(filter (\<lambda>x. x=b) w) + 1 \<longrightarrow> w \<in> A) \<and>
- (size(filter (\<lambda>x. x=b) w) = size(filter (\<lambda>x. x=a) w) + 1 \<longrightarrow> w \<in> B)"
+ "(size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b] \<longrightarrow> w \<in> S) \<and>
+ (size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b] + 1 \<longrightarrow> w \<in> A) \<and>
+ (size[x\<leftarrow>w. x=b] = size[x\<leftarrow>w. x=a] + 1 \<longrightarrow> w \<in> B)"
txt\<open>\noindent
The proof is by induction on @{term w}. Structural induction would fail here
@@ -232,9 +234,9 @@
apply(clarify)
txt\<open>\noindent
This yields an index @{prop"i \<le> length v"} such that
-@{prop[display]"length (filter (\<lambda>x. x=a) (take i v)) = length (filter (\<lambda>x. x=b) (take i v)) + 1"}
+@{prop[display]"length [x\<leftarrow>take i v . x = a] = length [x\<leftarrow>take i v . x = b] + 1"}
With the help of @{thm[source]part2} it follows that
-@{prop[display]"length (filter (\<lambda>x. x=a) (drop i v)) = length (filter (\<lambda>x. x=b) (drop i v)) + 1"}
+@{prop[display]"length [x\<leftarrow>drop i v . x = a] = length [x\<leftarrow>drop i v . x = b] + 1"}
\<close>
apply(drule part2[of "\<lambda>x. x=a", simplified])
--- a/src/HOL/HOLCF/Cfun.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/HOLCF/Cfun.thy Wed Jun 06 14:27:10 2018 +0100
@@ -394,7 +394,7 @@
lemma flat_codom: "f\<cdot>x = c \<Longrightarrow> f\<cdot>\<bottom> = \<bottom> \<or> (\<forall>z. f\<cdot>z = c)"
for c :: "'b::flat"
- apply (case_tac "f\<cdot>x = \<bottom>")
+ apply (cases "f\<cdot>x = \<bottom>")
apply (rule disjI1)
apply (rule bottomI)
apply (erule_tac t="\<bottom>" in subst)
--- a/src/HOL/HOLCF/Completion.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/HOLCF/Completion.thy Wed Jun 06 14:27:10 2018 +0100
@@ -41,13 +41,13 @@
unfolding ideal_def by fast
lemma ideal_principal: "ideal {x. x \<preceq> z}"
-apply (rule idealI)
-apply (rule_tac x=z in exI)
-apply (fast intro: r_refl)
-apply (rule_tac x=z in bexI, fast)
-apply (fast intro: r_refl)
-apply (fast intro: r_trans)
-done
+ apply (rule idealI)
+ apply (rule exI [where x = z])
+ apply (fast intro: r_refl)
+ apply (rule bexI [where x = z], fast)
+ apply (fast intro: r_refl)
+ apply (fast intro: r_trans)
+ done
lemma ex_ideal: "\<exists>A. A \<in> {A. ideal A}"
by (fast intro: ideal_principal)
@@ -59,17 +59,19 @@
assumes ideal_A: "\<And>i. ideal (A i)"
assumes chain_A: "\<And>i j. i \<le> j \<Longrightarrow> A i \<subseteq> A j"
shows "ideal (\<Union>i. A i)"
- apply (rule idealI)
- apply (cut_tac idealD1 [OF ideal_A], fast)
- apply (clarify, rename_tac i j)
- apply (drule subsetD [OF chain_A [OF max.cobounded1]])
- apply (drule subsetD [OF chain_A [OF max.cobounded2]])
- apply (drule (1) idealD2 [OF ideal_A])
- apply blast
- apply clarify
- apply (drule (1) idealD3 [OF ideal_A])
- apply fast
-done
+ apply (rule idealI)
+ using idealD1 [OF ideal_A] apply fast
+ apply (clarify)
+ subgoal for i j
+ apply (drule subsetD [OF chain_A [OF max.cobounded1]])
+ apply (drule subsetD [OF chain_A [OF max.cobounded2]])
+ apply (drule (1) idealD2 [OF ideal_A])
+ apply blast
+ done
+ apply clarify
+ apply (drule (1) idealD3 [OF ideal_A])
+ apply fast
+ done
lemma typedef_ideal_po:
fixes Abs :: "'a set \<Rightarrow> 'b::below"
@@ -208,10 +210,10 @@
have a_mem: "enum a \<in> rep x"
unfolding a_def
apply (rule LeastI_ex)
- apply (cut_tac ideal_rep [of x])
+ apply (insert ideal_rep [of x])
apply (drule idealD1)
- apply (clarify, rename_tac a)
- apply (rule_tac x="count a" in exI, simp)
+ apply (clarify)
+ subgoal for a by (rule exI [where x="count a"]) simp
done
have b: "\<And>i. P i \<Longrightarrow> enum i \<in> rep x
\<Longrightarrow> enum (b i) \<in> rep x \<and> \<not> enum (b i) \<preceq> enum i"
@@ -220,50 +222,63 @@
\<Longrightarrow> enum (c i j) \<in> rep x \<and> enum i \<preceq> enum (c i j) \<and> enum j \<preceq> enum (c i j)"
unfolding c_def
apply (drule (1) idealD2 [OF ideal_rep], clarify)
- apply (rule_tac a="count z" in LeastI2, simp, simp)
+ subgoal for \<dots> z by (rule LeastI2 [where a="count z"], simp, simp)
done
- have X_mem: "\<And>n. enum (X n) \<in> rep x"
- apply (induct_tac n)
- apply (simp add: X_0 a_mem)
- apply (clarsimp simp add: X_Suc, rename_tac n)
- apply (simp add: b c)
- done
+ have X_mem: "enum (X n) \<in> rep x" for n
+ proof (induct n)
+ case 0
+ then show ?case by (simp add: X_0 a_mem)
+ next
+ case (Suc n)
+ with b c show ?case by (auto simp: X_Suc)
+ qed
have X_chain: "\<And>n. enum (X n) \<preceq> enum (X (Suc n))"
apply (clarsimp simp add: X_Suc r_refl)
apply (simp add: b c X_mem)
done
have less_b: "\<And>n i. n < b i \<Longrightarrow> enum n \<in> rep x \<Longrightarrow> enum n \<preceq> enum i"
unfolding b_def by (drule not_less_Least, simp)
- have X_covers: "\<And>n. \<forall>k\<le>n. enum k \<in> rep x \<longrightarrow> enum k \<preceq> enum (X n)"
- apply (induct_tac n)
- apply (clarsimp simp add: X_0 a_def)
- apply (drule_tac k=0 in Least_le, simp add: r_refl)
- apply (clarsimp, rename_tac n k)
- apply (erule le_SucE)
- apply (rule r_trans [OF _ X_chain], simp)
- apply (case_tac "P (X n)", simp add: X_Suc)
- apply (rule_tac x="b (X n)" and y="Suc n" in linorder_cases)
- apply (simp only: less_Suc_eq_le)
- apply (drule spec, drule (1) mp, simp add: b X_mem)
- apply (simp add: c X_mem)
- apply (drule (1) less_b)
- apply (erule r_trans)
- apply (simp add: b c X_mem)
- apply (simp add: X_Suc)
- apply (simp add: P_def)
- done
+ have X_covers: "\<forall>k\<le>n. enum k \<in> rep x \<longrightarrow> enum k \<preceq> enum (X n)" for n
+ proof (induct n)
+ case 0
+ then show ?case
+ apply (clarsimp simp add: X_0 a_def)
+ apply (drule Least_le [where k=0], simp add: r_refl)
+ done
+ next
+ case (Suc n)
+ then show ?case
+ apply clarsimp
+ apply (erule le_SucE)
+ apply (rule r_trans [OF _ X_chain], simp)
+ apply (cases "P (X n)", simp add: X_Suc)
+ apply (rule linorder_cases [where x="b (X n)" and y="Suc n"])
+ apply (simp only: less_Suc_eq_le)
+ apply (drule spec, drule (1) mp, simp add: b X_mem)
+ apply (simp add: c X_mem)
+ apply (drule (1) less_b)
+ apply (erule r_trans)
+ apply (simp add: b c X_mem)
+ apply (simp add: X_Suc)
+ apply (simp add: P_def)
+ done
+ qed
have 1: "\<forall>i. enum (X i) \<preceq> enum (X (Suc i))"
by (simp add: X_chain)
- have 2: "x = (\<Squnion>n. principal (enum (X n)))"
+ have "x = (\<Squnion>n. principal (enum (X n)))"
apply (simp add: eq_iff rep_lub 1 rep_principal)
- apply (auto, rename_tac a)
- apply (subgoal_tac "\<exists>i. a = enum i", erule exE)
- apply (rule_tac x=i in exI, simp add: X_covers)
- apply (rule_tac x="count a" in exI, simp)
- apply (erule idealD3 [OF ideal_rep])
- apply (rule X_mem)
+ apply auto
+ subgoal for a
+ apply (subgoal_tac "\<exists>i. a = enum i", erule exE)
+ apply (rule_tac x=i in exI, simp add: X_covers)
+ apply (rule_tac x="count a" in exI, simp)
+ done
+ subgoal
+ apply (erule idealD3 [OF ideal_rep])
+ apply (rule X_mem)
+ done
done
- from 1 2 show ?thesis ..
+ with 1 show ?thesis ..
qed
lemma principal_induct:
@@ -301,16 +316,20 @@
by (simp add: x rep_lub Y rep_principal)
have "f ` rep x <<| (\<Squnion>n. f (Y n))"
apply (rule is_lubI)
- apply (rule ub_imageI, rename_tac a)
- apply (clarsimp simp add: rep_x)
- apply (drule f_mono)
- apply (erule below_lub [OF chain])
+ apply (rule ub_imageI)
+ subgoal for a
+ apply (clarsimp simp add: rep_x)
+ apply (drule f_mono)
+ apply (erule below_lub [OF chain])
+ done
apply (rule lub_below [OF chain])
- apply (drule_tac x="Y n" in ub_imageD)
- apply (simp add: rep_x, fast intro: r_refl)
- apply assumption
+ subgoal for \<dots> n
+ apply (drule ub_imageD [where x="Y n"])
+ apply (simp add: rep_x, fast intro: r_refl)
+ apply assumption
+ done
done
- thus ?thesis ..
+ then show ?thesis ..
qed
lemma extension_beta:
@@ -353,16 +372,18 @@
assumes g_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> g a \<sqsubseteq> g b"
assumes below: "\<And>a. f a \<sqsubseteq> g a"
shows "extension f \<sqsubseteq> extension g"
- apply (rule cfun_belowI)
- apply (simp only: extension_beta f_mono g_mono)
- apply (rule is_lub_thelub_ex)
- apply (rule extension_lemma, erule f_mono)
- apply (rule ub_imageI, rename_tac a)
- apply (rule below_trans [OF below])
- apply (rule is_ub_thelub_ex)
- apply (rule extension_lemma, erule g_mono)
- apply (erule imageI)
-done
+ apply (rule cfun_belowI)
+ apply (simp only: extension_beta f_mono g_mono)
+ apply (rule is_lub_thelub_ex)
+ apply (rule extension_lemma, erule f_mono)
+ apply (rule ub_imageI)
+ subgoal for x a
+ apply (rule below_trans [OF below])
+ apply (rule is_ub_thelub_ex)
+ apply (rule extension_lemma, erule g_mono)
+ apply (erule imageI)
+ done
+ done
lemma cont_extension:
assumes f_mono: "\<And>a b x. a \<preceq> b \<Longrightarrow> f x a \<sqsubseteq> f x b"
--- a/src/HOL/HOLCF/Domain_Aux.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/HOLCF/Domain_Aux.thy Wed Jun 06 14:27:10 2018 +0100
@@ -199,32 +199,40 @@
assumes f: "decisive f"
assumes g: "decisive g"
shows "decisive (ssum_map\<cdot>f\<cdot>g)"
-apply (rule decisiveI, rename_tac s)
-apply (case_tac s, simp_all)
-apply (rule_tac x=x in decisive_cases [OF f], simp_all)
-apply (rule_tac x=y in decisive_cases [OF g], simp_all)
-done
+ apply (rule decisiveI)
+ subgoal for s
+ apply (cases s, simp_all)
+ apply (rule_tac x=x in decisive_cases [OF f], simp_all)
+ apply (rule_tac x=y in decisive_cases [OF g], simp_all)
+ done
+ done
lemma decisive_sprod_map:
assumes f: "decisive f"
assumes g: "decisive g"
shows "decisive (sprod_map\<cdot>f\<cdot>g)"
-apply (rule decisiveI, rename_tac s)
-apply (case_tac s, simp_all)
-apply (rule_tac x=x in decisive_cases [OF f], simp_all)
-apply (rule_tac x=y in decisive_cases [OF g], simp_all)
-done
+ apply (rule decisiveI)
+ subgoal for s
+ apply (cases s, simp)
+ subgoal for x y
+ apply (rule decisive_cases [OF f, where x = x], simp_all)
+ apply (rule decisive_cases [OF g, where x = y], simp_all)
+ done
+ done
+ done
lemma decisive_abs_rep:
fixes abs rep
assumes iso: "iso abs rep"
assumes d: "decisive d"
shows "decisive (abs oo d oo rep)"
-apply (rule decisiveI)
-apply (rule_tac x="rep\<cdot>x" in decisive_cases [OF d])
-apply (simp add: iso.rep_iso [OF iso])
-apply (simp add: iso.abs_strict [OF iso])
-done
+ apply (rule decisiveI)
+ subgoal for s
+ apply (rule decisive_cases [OF d, where x="rep\<cdot>s"])
+ apply (simp add: iso.rep_iso [OF iso])
+ apply (simp add: iso.abs_strict [OF iso])
+ done
+ done
lemma lub_ID_finite:
assumes chain: "chain d"
--- a/src/HOL/Library/AList.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/Library/AList.thy Wed Jun 06 14:27:10 2018 +0100
@@ -45,7 +45,7 @@
using assms by (simp add: update_keys)
lemma update_filter:
- "a \<noteq> k \<Longrightarrow> update k v (filter (\<lambda>q. fst q \<noteq> a) ps) = filter (\<lambda>q. fst q \<noteq> a) (update k v ps)"
+ "a \<noteq> k \<Longrightarrow> update k v [q\<leftarrow>ps. fst q \<noteq> a] = [q\<leftarrow>update k v ps. fst q \<noteq> a]"
by (induct ps) auto
lemma update_triv: "map_of al k = Some v \<Longrightarrow> update k v al = al"
@@ -361,12 +361,12 @@
proof -
have "y \<noteq> x \<longleftrightarrow> x \<noteq> y" for y
by auto
- then show "filter (\<lambda>p. fst p \<in> D \<and> x \<noteq> fst p) al = filter (\<lambda>p. fst p \<in> D \<and> fst p \<noteq> x) al"
+ then show "[p \<leftarrow> al. fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al. fst p \<in> D \<and> fst p \<noteq> x]"
by simp
assume "x \<notin> D"
then have "y \<in> D \<longleftrightarrow> y \<in> D \<and> x \<noteq> y" for y
by auto
- then show "filter (\<lambda>p. fst p \<in> D \<and> x \<noteq> fst p) al = filter (\<lambda>p. fst p \<in> D) al"
+ then show "[p \<leftarrow> al . fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al . fst p \<in> D]"
by simp
qed
@@ -492,7 +492,7 @@
lemma distinct_map_ran: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
by (simp add: map_ran_def split_def comp_def)
-lemma map_ran_filter: "map_ran f (filter (\<lambda>p. fst p \<noteq> a) ps) = filter (\<lambda>p. fst p \<noteq> a) (map_ran f ps)"
+lemma map_ran_filter: "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]"
by (simp add: map_ran_def filter_map split_def comp_def)
lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
--- a/src/HOL/Library/Code_Lazy.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/Library/Code_Lazy.thy Wed Jun 06 14:27:10 2018 +0100
@@ -17,7 +17,7 @@
text \<open>
This theory and the CodeLazy tool described in @{cite "LochbihlerStoop2018"}.
- It hooks into Isabelle’s code generator such that the generated code evaluates a user-specified
+ It hooks into Isabelle's code generator such that the generated code evaluates a user-specified
set of type constructors lazily, even in target languages with eager evaluation.
The lazy type must be algebraic, i.e., values must be built from constructors and a
corresponding case operator decomposes them. Every datatype and codatatype is algebraic
--- a/src/HOL/Library/Finite_Map.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/Library/Finite_Map.thy Wed Jun 06 14:27:10 2018 +0100
@@ -84,10 +84,10 @@
definition map_filter :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
"map_filter P m = (\<lambda>x. if P x then m x else None)"
-lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of (filter (\<lambda>(k, _). P k) m)"
+lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of [(k, _) \<leftarrow> m. P k]"
proof
fix x
- show "map_filter P (map_of m) x = map_of (filter (\<lambda>(k, _). P k) m) x"
+ show "map_filter P (map_of m) x = map_of [(k, _) \<leftarrow> m. P k] x"
by (induct m) (auto simp: map_filter_def)
qed
--- a/src/HOL/Library/Multiset.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/Library/Multiset.thy Wed Jun 06 14:27:10 2018 +0100
@@ -1888,7 +1888,7 @@
apply simp
done
-lemma mset_compl_union [simp]: "mset (filter P xs) + mset (filter (\<lambda>x. \<not>P x) xs) = mset xs"
+lemma mset_compl_union [simp]: "mset [x\<leftarrow>xs. P x] + mset [x\<leftarrow>xs. \<not>P x] = mset xs"
by (induct xs) auto
lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) \<in># mset ls"
@@ -2582,14 +2582,14 @@
show "mset ys = mset xs" by simp
from \<open>sorted (map f ys)\<close>
show "sorted (map f ys)" .
- show "filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs" if "k \<in> set ys" for k
+ show "[x\<leftarrow>ys . f k = f x] = [x\<leftarrow>xs . f k = f x]" if "k \<in> set ys" for k
proof -
from mset_equal
have set_equal: "set xs = set ys" by (rule mset_eq_setD)
with that have "insert k (set ys) = set ys" by auto
with \<open>inj_on f (set xs)\<close> have inj: "inj_on f (insert k (set ys))"
by (simp add: set_equal)
- from inj have "filter (\<lambda>x. f k = f x) ys = filter (HOL.eq k) ys"
+ from inj have "[x\<leftarrow>ys . f k = f x] = filter (HOL.eq k) ys"
by (auto intro!: inj_on_filter_key_eq)
also have "\<dots> = replicate (count (mset ys) k) k"
by (simp add: replicate_count_mset_eq_filter_eq)
@@ -2597,7 +2597,7 @@
using mset_equal by simp
also have "\<dots> = filter (HOL.eq k) xs"
by (simp add: replicate_count_mset_eq_filter_eq)
- also have "\<dots> = filter (\<lambda>x. f k = f x) xs"
+ also have "\<dots> = [x\<leftarrow>xs . f k = f x]"
using inj by (auto intro!: inj_on_filter_key_eq [symmetric] simp add: set_equal)
finally show ?thesis .
qed
@@ -2610,9 +2610,9 @@
by (rule sort_key_inj_key_eq) (simp_all add: assms)
lemma sort_key_by_quicksort:
- "sort_key f xs = sort_key f (filter (\<lambda>x. f x < f (xs ! (length xs div 2))) xs)
- @ filter (\<lambda>x. f x = f (xs ! (length xs div 2))) xs
- @ sort_key f (filter (\<lambda>x. f x > f (xs ! (length xs div 2))) xs)" (is "sort_key f ?lhs = ?rhs")
+ "sort_key f xs = sort_key f [x\<leftarrow>xs. f x < f (xs ! (length xs div 2))]
+ @ [x\<leftarrow>xs. f x = f (xs ! (length xs div 2))]
+ @ sort_key f [x\<leftarrow>xs. f x > f (xs ! (length xs div 2))]" (is "sort_key f ?lhs = ?rhs")
proof (rule properties_for_sort_key)
show "mset ?rhs = mset ?lhs"
by (rule multiset_eqI) (auto simp add: mset_filter)
@@ -2623,14 +2623,14 @@
assume "l \<in> set ?rhs"
let ?pivot = "f (xs ! (length xs div 2))"
have *: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto
- have "filter (\<lambda>x. f x = f l) (sort_key f xs) = filter (\<lambda>x. f x = f l) xs"
+ have "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]"
unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same)
- with * have **: "filter (\<lambda>x. f l = f x) (sort_key f xs) = filter (\<lambda>x. f l = f x) xs" by simp
+ with * have **: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp
have "\<And>x P. P (f x) ?pivot \<and> f l = f x \<longleftrightarrow> P (f l) ?pivot \<and> f l = f x" by auto
- then have "\<And>P. filter (\<lambda>x. P (f x) ?pivot \<and> f l = f x) (sort_key f xs) =
- filter (\<lambda>x. P (f l) ?pivot \<and> f l = f x) (sort_key f xs)" by simp
+ then have "\<And>P. [x \<leftarrow> sort_key f xs . P (f x) ?pivot \<and> f l = f x] =
+ [x \<leftarrow> sort_key f xs. P (f l) ?pivot \<and> f l = f x]" by simp
note *** = this [of "(<)"] this [of "(>)"] this [of "(=)"]
- show "filter (\<lambda>x. f l = f x) ?rhs = filter (\<lambda>x. f l = f x) ?lhs"
+ show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]"
proof (cases "f l" ?pivot rule: linorder_cases)
case less
then have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto
@@ -2648,15 +2648,15 @@
qed
lemma sort_by_quicksort:
- "sort xs = sort (filter (\<lambda>x. x < xs ! (length xs div 2)) xs)
- @ filter (\<lambda>x. x = xs ! (length xs div 2)) xs
- @ sort (filter (\<lambda>x. x > xs ! (length xs div 2)) xs)" (is "sort ?lhs = ?rhs")
+ "sort xs = sort [x\<leftarrow>xs. x < xs ! (length xs div 2)]
+ @ [x\<leftarrow>xs. x = xs ! (length xs div 2)]
+ @ sort [x\<leftarrow>xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs")
using sort_key_by_quicksort [of "\<lambda>x. x", symmetric] by simp
text \<open>A stable parametrized quicksort\<close>
definition part :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'b list \<times> 'b list \<times> 'b list" where
- "part f pivot xs = (filter (\<lambda>x. f x < pivot) xs, filter (\<lambda>x. f x = pivot) xs, filter (\<lambda>x. f x > pivot) xs)"
+ "part f pivot xs = ([x \<leftarrow> xs. f x < pivot], [x \<leftarrow> xs. f x = pivot], [x \<leftarrow> xs. pivot < f x])"
lemma part_code [code]:
"part f pivot [] = ([], [], [])"
--- a/src/HOL/MicroJava/DFA/Kildall.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/MicroJava/DFA/Kildall.thy Wed Jun 06 14:27:10 2018 +0100
@@ -38,7 +38,7 @@
lemma (in Semilat) nth_merges:
"\<And>ss. \<lbrakk>p < length ss; ss \<in> list n A; \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
- (merges f ps ss)!p = map snd (filter (\<lambda>(p',t'). p'=p) ps) ++_f ss!p"
+ (merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] ++_f ss!p"
(is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")
proof (induct ps)
show "\<And>ss. ?P ss []" by simp
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy Wed Jun 06 14:27:10 2018 +0100
@@ -80,13 +80,13 @@
assume merge: "?s1 \<noteq> T"
from x ss1 have "?s1 =
(if \<forall>(pc', s')\<in>set ss1. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
- then (map snd (filter (\<lambda>(p', t'). p'=pc+1) ss1)) ++_f x
+ then (map snd [(p', t') \<leftarrow> ss1 . p'=pc+1]) ++_f x
else \<top>)"
by (rule merge_def)
with merge obtain
app: "\<forall>(pc',s')\<in>set ss1. pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc'"
(is "?app ss1") and
- sum: "(map snd (filter (\<lambda>(p',t'). p' = pc+1) ss1) ++_f x) = ?s1"
+ sum: "(map snd [(p',t') \<leftarrow> ss1 . p' = pc+1] ++_f x) = ?s1"
(is "?map ss1 ++_f x = _" is "?sum ss1 = _")
by (simp split: if_split_asm)
from app less
@@ -115,7 +115,7 @@
from x ss2 have
"?s2 =
(if \<forall>(pc', s')\<in>set ss2. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
- then map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss2) ++_f x
+ then map snd [(p', t') \<leftarrow> ss2 . p' = pc + 1] ++_f x
else \<top>)"
by (rule merge_def)
ultimately have ?thesis by simp
@@ -194,7 +194,7 @@
ultimately
have "merge c pc ?step (c!Suc pc) =
(if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'
- then map snd (filter (\<lambda>(p',t').p'=pc+1) ?step) ++_f c!Suc pc
+ then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc
else \<top>)" unfolding mrg_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms])
moreover {
fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"
@@ -207,7 +207,7 @@
} hence "\<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto
moreover
from pc have "Suc pc = length \<phi> \<or> Suc pc < length \<phi>" by auto
- hence "map snd (filter (\<lambda>(p',t').p'=pc+1) ?step) ++_f c!Suc pc \<noteq> \<top>"
+ hence "map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc \<noteq> \<top>"
(is "?map ++_f _ \<noteq> _")
proof (rule disjE)
assume pc': "Suc pc = length \<phi>"
@@ -215,7 +215,7 @@
moreover
from pc' bounded pc
have "\<forall>(p',t')\<in>set ?step. p'\<noteq>pc+1" by clarify (drule boundedD, auto)
- hence "filter (\<lambda>(p',t').p'=pc+1) ?step = []" by (blast intro: filter_False)
+ hence "[(p',t') \<leftarrow> ?step.p'=pc+1] = []" by (blast intro: filter_False)
hence "?map = []" by simp
ultimately show ?thesis by (simp add: B_neq_T)
next
@@ -262,7 +262,7 @@
hence "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by (simp add: wti)
ultimately
have "merge c pc ?step (c!Suc pc) =
- map snd (filter (\<lambda>(p',t').p'=pc+1) ?step) ++_f c!Suc pc" by (rule merge_not_top_s)
+ map snd [(p',t')\<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc" by (rule merge_not_top_s)
hence "?wti = \<dots>" (is "_ = (?map ++_f _)" is "_ = ?sum") by (simp add: wti)
also {
from suc_pc phi have "\<phi>!Suc pc \<in> A" by simp
--- a/src/HOL/MicroJava/DFA/LBVCorrect.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/MicroJava/DFA/LBVCorrect.thy Wed Jun 06 14:27:10 2018 +0100
@@ -88,7 +88,7 @@
also
from s2 merge have "\<dots> \<noteq> \<top>" (is "?merge \<noteq> _") by simp
with cert_in_A step_in_A
- have "?merge = (map snd (filter (\<lambda>(p',t').p'=pc+1) (?step pc)) ++_f (c!(pc+1)))"
+ have "?merge = (map snd [(p',t') \<leftarrow> ?step pc. p'=pc+1] ++_f (c!(pc+1)))"
by (rule merge_not_top_s)
finally
have "s' <=_r ?s2" using step_in_A cert_in_A True step
--- a/src/HOL/MicroJava/DFA/LBVSpec.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/MicroJava/DFA/LBVSpec.thy Wed Jun 06 14:27:10 2018 +0100
@@ -113,7 +113,7 @@
lemma (in Semilat) pp_ub1':
assumes S: "snd`set S \<subseteq> A"
assumes y: "y \<in> A" and ab: "(a, b) \<in> set S"
- shows "b <=_r map snd (filter (\<lambda>(p', t'). p' = a) S) ++_f y"
+ shows "b <=_r map snd [(p', t') \<leftarrow> S . p' = a] ++_f y"
proof -
from S have "\<forall>(x,y) \<in> set S. y \<in> A" by auto
with semilat y ab show ?thesis by - (rule ub1')
@@ -172,7 +172,7 @@
"\<And>x. x \<in> A \<Longrightarrow> snd`set ss \<subseteq> A \<Longrightarrow>
merge c pc ss x =
(if \<forall>(pc',s') \<in> set ss. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc' then
- map snd (filter (\<lambda>(p',t'). p'=pc+1) ss) ++_f x
+ map snd [(p',t') \<leftarrow> ss. p'=pc+1] ++_f x
else \<top>)"
(is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?merge ss x = ?if ss x" is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?P ss x")
proof (induct ss)
@@ -202,15 +202,15 @@
hence "\<forall>(pc', s')\<in>set ls. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto
moreover
from True have
- "map snd (filter (\<lambda>(p',t'). p'=pc+1) ls) ++_f ?if' =
- (map snd (filter (\<lambda>(p',t'). p'=pc+1) (l#ls)) ++_f x)"
+ "map snd [(p',t')\<leftarrow>ls . p'=pc+1] ++_f ?if' =
+ (map snd [(p',t')\<leftarrow>l#ls . p'=pc+1] ++_f x)"
by simp
ultimately
show ?thesis using True by simp
next
case False
moreover
- from ls have "set (map snd (filter (\<lambda>(p', t'). p' = Suc pc) ls)) \<subseteq> A" by auto
+ from ls have "set (map snd [(p', t')\<leftarrow>ls . p' = Suc pc]) \<subseteq> A" by auto
ultimately show ?thesis by auto
qed
finally show "?P (l#ls) x" .
@@ -219,7 +219,7 @@
lemma (in lbv) merge_not_top_s:
assumes x: "x \<in> A" and ss: "snd`set ss \<subseteq> A"
assumes m: "merge c pc ss x \<noteq> \<top>"
- shows "merge c pc ss x = (map snd (filter (\<lambda>(p',t'). p'=pc+1) ss) ++_f x)"
+ shows "merge c pc ss x = (map snd [(p',t') \<leftarrow> ss. p'=pc+1] ++_f x)"
proof -
from ss m have "\<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc')"
by (rule merge_not_top)
@@ -307,8 +307,8 @@
assumes s0: "snd`set ss \<subseteq> A" and x: "x \<in> A"
shows "merge c pc ss x \<in> A"
proof -
- from s0 have "set (map snd (filter (\<lambda>(p', t'). p'=pc+1) ss)) \<subseteq> A" by auto
- with x have "(map snd (filter (\<lambda>(p', t'). p'=pc+1) ss) ++_f x) \<in> A"
+ from s0 have "set (map snd [(p', t')\<leftarrow>ss . p'=pc+1]) \<subseteq> A" by auto
+ with x have "(map snd [(p', t')\<leftarrow>ss . p'=pc+1] ++_f x) \<in> A"
by (auto intro!: plusplus_closed semilat)
with s0 x show ?thesis by (simp add: merge_def T_A)
qed
--- a/src/HOL/MicroJava/DFA/SemilatAlg.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/MicroJava/DFA/SemilatAlg.thy Wed Jun 06 14:27:10 2018 +0100
@@ -155,7 +155,7 @@
lemma ub1':
assumes "semilat (A, r, f)"
shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk>
- \<Longrightarrow> b <=_r map snd (filter (\<lambda>(p', t'). p' = a) S) ++_f y"
+ \<Longrightarrow> b <=_r map snd [(p', t')\<leftarrow>S. p' = a] ++_f y"
proof -
interpret Semilat A r f using assms by (rule Semilat.intro)
@@ -175,7 +175,7 @@
lemma plusplus_empty:
"\<forall>s'. (q, s') \<in> set S \<longrightarrow> s' +_f ss ! q = ss ! q \<Longrightarrow>
- (map snd (filter (\<lambda>(p', t'). p' = q) S) ++_f ss ! q) = ss ! q"
+ (map snd [(p', t') \<leftarrow> S. p' = q] ++_f ss ! q) = ss ! q"
by (induct S) auto
end
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Jun 06 14:27:10 2018 +0100
@@ -317,7 +317,7 @@
| "\<lbrakk>v \<in> B\<^sub>1; v \<in> B\<^sub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>1"
theorem S\<^sub>1_sound:
-"w \<in> S\<^sub>1 \<longrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
+"w \<in> S\<^sub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
nitpick [expect = genuine]
oops
@@ -330,7 +330,7 @@
| "\<lbrakk>v \<in> B\<^sub>2; v \<in> B\<^sub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>2"
theorem S\<^sub>2_sound:
-"w \<in> S\<^sub>2 \<longrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
+"w \<in> S\<^sub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
nitpick [expect = genuine]
oops
@@ -343,12 +343,12 @@
| "\<lbrakk>v \<in> B\<^sub>3; w \<in> B\<^sub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>3"
theorem S\<^sub>3_sound:
-"w \<in> S\<^sub>3 \<longrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
+"w \<in> S\<^sub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
nitpick [card = 1-5, expect = none]
sorry
theorem S\<^sub>3_complete:
-"length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w) \<longrightarrow> w \<in> S\<^sub>3"
+"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>3"
nitpick [expect = genuine]
oops
@@ -362,19 +362,19 @@
| "\<lbrakk>v \<in> B\<^sub>4; w \<in> B\<^sub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>4"
theorem S\<^sub>4_sound:
-"w \<in> S\<^sub>4 \<longrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
+"w \<in> S\<^sub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
nitpick [card = 1-5, expect = none]
sorry
theorem S\<^sub>4_complete:
-"length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w) \<longrightarrow> w \<in> S\<^sub>4"
+"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>4"
nitpick [card = 1-5, expect = none]
sorry
theorem S\<^sub>4_A\<^sub>4_B\<^sub>4_sound_and_complete:
-"w \<in> S\<^sub>4 \<longleftrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
-"w \<in> A\<^sub>4 \<longleftrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w) + 1"
-"w \<in> B\<^sub>4 \<longleftrightarrow> length (filter (\<lambda>x. x = b) w) = length (filter (\<lambda>x. x = a) w) + 1"
+"w \<in> S\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+"w \<in> A\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
+"w \<in> B\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
nitpick [card = 1-5, expect = none]
sorry
--- a/src/HOL/Nominal/Examples/W.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/Nominal/Examples/W.thy Wed Jun 06 14:27:10 2018 +0100
@@ -9,7 +9,7 @@
abbreviation
"difference_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_ - _" [60,60] 60)
where
- "xs - ys \<equiv> filter (\<lambda>x. x\<notin>set ys) xs"
+ "xs - ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"
lemma difference_eqvt_tvar[eqvt]:
fixes pi::"tvar prm"
--- a/src/HOL/Parity.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/Parity.thy Wed Jun 06 14:27:10 2018 +0100
@@ -933,7 +933,7 @@
lemma drop_bit_of_nat:
"drop_bit n (of_nat m) = of_nat (drop_bit n m)"
- by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
+ by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
end
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Wed Jun 06 14:27:10 2018 +0100
@@ -71,7 +71,7 @@
oops
theorem S\<^sub>1_sound:
-"S\<^sub>1p w \<Longrightarrow> length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w)"
+"S\<^sub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
quickcheck[tester=smart_exhaustive, size=15]
oops
@@ -113,7 +113,7 @@
oops
*)
theorem S\<^sub>2_sound:
-"S\<^sub>2p w \<longrightarrow> length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w)"
+"S\<^sub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
quickcheck[tester=smart_exhaustive, size=5, iterations=10]
oops
@@ -133,16 +133,16 @@
lemma S\<^sub>3_sound:
-"S\<^sub>3p w \<longrightarrow> length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w)"
+"S\<^sub>3p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
quickcheck[tester=smart_exhaustive, size=10, iterations=10]
oops
-lemma "\<not> (length w > 2) \<or> \<not> (length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w))"
+lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])"
quickcheck[size=10, tester = smart_exhaustive]
oops
theorem S\<^sub>3_complete:
-"length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w) \<longrightarrow> S\<^sub>3p w"
+"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. b = x] \<longrightarrow> S\<^sub>3p w"
(*quickcheck[generator=SML]*)
quickcheck[tester=smart_exhaustive, size=10, iterations=100]
oops
@@ -158,12 +158,12 @@
| "\<lbrakk>v \<in> B\<^sub>4; w \<in> B\<^sub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>4"
theorem S\<^sub>4_sound:
-"S\<^sub>4p w \<longrightarrow> length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w)"
+"S\<^sub>4p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
quickcheck[tester = smart_exhaustive, size=5, iterations=1]
oops
theorem S\<^sub>4_complete:
-"length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w) \<longrightarrow> S\<^sub>4p w"
+"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> S\<^sub>4p w"
quickcheck[tester = smart_exhaustive, size=5, iterations=1]
oops
@@ -301,7 +301,7 @@
subsection "Compressed matrix"
-definition "sparsify xs = filter (\<lambda>i. snd i \<noteq> 0) (zip [0..<length xs] xs)"
+definition "sparsify xs = [i \<leftarrow> zip [0..<length xs] xs. snd i \<noteq> 0]"
(*
lemma sparsify_length: "(i, x) \<in> set (sparsify xs) \<Longrightarrow> i < length xs"
by (auto simp: sparsify_def set_zip)
--- a/src/HOL/Probability/Probability_Mass_Function.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Wed Jun 06 14:27:10 2018 +0100
@@ -2028,7 +2028,7 @@
private lemma pmf_of_list_aux:
assumes "\<And>x. x \<in> set (map snd xs) \<Longrightarrow> x \<ge> 0"
assumes "sum_list (map snd xs) = 1"
- shows "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) = 1"
+ shows "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])) \<partial>count_space UNIV) = 1"
proof -
have "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) =
(\<integral>\<^sup>+ x. ennreal (sum_list (map (\<lambda>(x',p). indicator {x'} x * p) xs)) \<partial>count_space UNIV)"
@@ -2083,7 +2083,7 @@
show "x \<in> set (map fst xs)"
proof (rule ccontr)
assume "x \<notin> set (map fst xs)"
- hence "filter (\<lambda>z. fst z = x) xs = []" by (auto simp: filter_empty_conv)
+ hence "[z\<leftarrow>xs . fst z = x] = []" by (auto simp: filter_empty_conv)
with A assms show False by (simp add: pmf_pmf_of_list set_pmf_eq)
qed
qed
@@ -2122,10 +2122,10 @@
have "emeasure (pmf_of_list xs) A = nn_integral (measure_pmf (pmf_of_list xs)) (indicator A)"
by simp
also from assms
- have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (sum_list (map snd (filter (\<lambda>z. fst z = x) xs))))"
+ have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])))"
by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list Int_def)
also from assms
- have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
+ have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. sum_list (map snd [z\<leftarrow>xs . fst z = x]))"
by (subst sum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg)
also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A.
indicator A x * pmf (pmf_of_list xs) x)" (is "_ = ennreal ?S")
@@ -2184,7 +2184,7 @@
{
fix x assume A: "x \<in> fst ` set xs" and B: "x \<notin> set_pmf (pmf_of_list xs)"
then obtain y where y: "(x, y) \<in> set xs" by auto
- from B have "sum_list (map snd (filter (\<lambda>z. fst z = x) xs)) = 0"
+ from B have "sum_list (map snd [z\<leftarrow>xs. fst z = x]) = 0"
by (simp add: pmf_pmf_of_list[OF assms(1)] set_pmf_eq)
moreover from y have "y \<in> snd ` {xa \<in> set xs. fst xa = x}" by force
ultimately have "y = 0" using assms(1)
@@ -2199,11 +2199,11 @@
defines "xs' \<equiv> filter (\<lambda>z. snd z \<noteq> 0) xs"
shows "pmf_of_list_wf xs'" "pmf_of_list xs' = pmf_of_list xs"
proof -
- have "map snd (filter (\<lambda>z. snd z \<noteq> 0) xs) = filter (\<lambda>x. x \<noteq> 0) (map snd xs)"
+ have "map snd [z\<leftarrow>xs . snd z \<noteq> 0] = filter (\<lambda>x. x \<noteq> 0) (map snd xs)"
by (induction xs) simp_all
with assms(1) show wf: "pmf_of_list_wf xs'"
by (auto simp: pmf_of_list_wf_def xs'_def sum_list_filter_nonzero)
- have "sum_list (map snd (filter (\<lambda>z. fst z = i) xs')) = sum_list (map snd (filter (\<lambda>z. fst z = i) xs))" for i
+ have "sum_list (map snd [z\<leftarrow>xs' . fst z = i]) = sum_list (map snd [z\<leftarrow>xs . fst z = i])" for i
unfolding xs'_def by (induction xs) simp_all
with assms(1) wf show "pmf_of_list xs' = pmf_of_list xs"
by (intro pmf_eqI) (simp_all add: pmf_pmf_of_list)
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Wed Jun 06 14:27:10 2018 +0100
@@ -186,7 +186,7 @@
oops
lemma
- "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) (filter (\<lambda>ys. i < length ys) xs)"
+ "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<-xs. i < length ys]"
quickcheck[random, iterations = 10000]
quickcheck[exhaustive, expect = counterexample]
oops
@@ -228,13 +228,13 @@
oops
lemma
- "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) (filter (\<lambda>ys. i < length ys) (remdups xs))"
+ "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-remdups xs. i < length ys]"
quickcheck[random]
quickcheck[exhaustive, expect = counterexample]
oops
lemma
- "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) (filter (\<lambda>ys. length ys \<in> {..<i}) (List.transpose xs))"
+ "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. length ys \<in> {..<i}]"
quickcheck[random]
quickcheck[exhaustive, expect = counterexample]
oops
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy Wed Jun 06 14:27:10 2018 +0100
@@ -69,12 +69,12 @@
definition
inter_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
- [simp]: "inter_list xs ys = filter (\<lambda>x. x \<in> set xs \<and> x \<in> set ys) xs"
+ [simp]: "inter_list xs ys = [x \<leftarrow> xs. x \<in> set xs \<and> x \<in> set ys]"
definition
diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
- [simp]: "diff_list xs ys = filter (\<lambda>x. x \<notin> set ys) xs"
+ [simp]: "diff_list xs ys = [x \<leftarrow> xs. x \<notin> set ys]"
definition
rsp_fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
--- a/src/HOL/Random.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/Random.thy Wed Jun 06 14:27:10 2018 +0100
@@ -116,7 +116,7 @@
lemma select_weight_drop_zero:
"select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
proof -
- have "sum_list (map fst (filter (\<lambda>(k, _). 0 < k) xs)) = sum_list (map fst xs)"
+ have "sum_list (map fst [(k, _)\<leftarrow>xs . 0 < k]) = sum_list (map fst xs)"
by (induct xs) (auto simp add: less_natural_def natural_eq_iff)
then show ?thesis by (simp only: select_weight_def pick_drop_zero)
qed
--- a/src/HOL/Real_Vector_Spaces.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Wed Jun 06 14:27:10 2018 +0100
@@ -70,7 +70,7 @@
apply (force simp add: linear_def real_scaleR_def[abs_def])
done
-hide_const (open)\<comment>\<open>locale constants\<close>
+hide_const (open)\<comment> \<open>locale constants\<close>
real_vector.dependent
real_vector.independent
real_vector.representation
@@ -89,7 +89,7 @@
unfolding linear_def real_scaleR_def
by (rule refl)+
-hide_const (open)\<comment>\<open>locale constants\<close>
+hide_const (open)\<comment> \<open>locale constants\<close>
real_vector.construct
lemma linear_compose: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (g o f)"
@@ -168,7 +168,7 @@
apply (erule (1) nonzero_inverse_scaleR_distrib)
done
-lemmas sum_constant_scaleR = real_vector.sum_constant_scale\<comment>\<open>legacy name\<close>
+lemmas sum_constant_scaleR = real_vector.sum_constant_scale\<comment> \<open>legacy name\<close>
named_theorems vector_add_divide_simps "to simplify sums of scaled vectors"
--- a/src/HOL/Vector_Spaces.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/Vector_Spaces.thy Wed Jun 06 14:27:10 2018 +0100
@@ -41,7 +41,7 @@
locale vector_space =
fixes scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
- assumes vector_space_assms:\<comment>\<open>re-stating the assumptions of \<open>module\<close> instead of extending \<open>module\<close>
+ assumes vector_space_assms:\<comment> \<open>re-stating the assumptions of \<open>module\<close> instead of extending \<open>module\<close>
allows us to rewrite in the sublocale.\<close>
"a *s (x + y) = a *s x + a *s y"
"(a + b) *s x = a *s x + b *s x"
@@ -68,7 +68,7 @@
sublocale module scale rewrites "module_hom = linear"
by (unfold_locales) (fact vector_space_assms module_hom_eq_linear)+
-lemmas\<comment>\<open>from \<open>module\<close>\<close>
+lemmas\<comment> \<open>from \<open>module\<close>\<close>
linear_id = module_hom_id
and linear_ident = module_hom_ident
and linear_scale_self = module_hom_scale_self
@@ -607,7 +607,7 @@
context fixes f assumes "linear s1 s2 f" begin
interpretation linear s1 s2 f by fact
-lemmas\<comment>\<open>from locale \<open>module_hom\<close>\<close>
+lemmas\<comment> \<open>from locale \<open>module_hom\<close>\<close>
linear_0 = zero
and linear_add = add
and linear_scale = scale
@@ -634,7 +634,7 @@
rewrites "module_hom = linear"
by unfold_locales (fact module_hom_eq_linear)
-lemmas\<comment>\<open>from locale \<open>module_pair\<close>\<close>
+lemmas\<comment> \<open>from locale \<open>module_pair\<close>\<close>
linear_eq_on_span = module_hom_eq_on_span
and linear_compose_scale_right = module_hom_scale
and linear_compose_add = module_hom_add
@@ -834,7 +834,7 @@
by (auto simp: that construct_in_span in_span_in_range_construct)
lemma linear_independent_extend_subspace:
- \<comment>\<open>legacy: use @{term construct} instead\<close>
+ \<comment> \<open>legacy: use @{term construct} instead\<close>
assumes "vs1.independent B"
shows "\<exists>g. linear s1 s2 g \<and> (\<forall>x\<in>B. g x = f x) \<and> range g = vs2.span (f`B)"
by (rule exI[where x="construct B f"])
--- a/src/HOL/ex/Quicksort.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/ex/Quicksort.thy Wed Jun 06 14:27:10 2018 +0100
@@ -13,11 +13,11 @@
fun quicksort :: "'a list \<Rightarrow> 'a list" where
"quicksort [] = []"
-| "quicksort (x#xs) = quicksort (filter (\<lambda>y. \<not> x\<le>y) xs) @ [x] @ quicksort (filter (\<lambda>y. x\<le>y) xs)"
+| "quicksort (x#xs) = quicksort [y\<leftarrow>xs. \<not> x\<le>y] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
lemma [code]:
"quicksort [] = []"
- "quicksort (x#xs) = quicksort (filter (\<lambda>y. \<not> x\<le>y) xs) @ [x] @ quicksort (filter (\<lambda>y. x\<le>y) xs)"
+ "quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
by (simp_all add: not_le)
lemma quicksort_permutes [simp]:
--- a/src/HOL/ex/Radix_Sort.thy Wed Jun 06 14:25:53 2018 +0100
+++ b/src/HOL/ex/Radix_Sort.thy Wed Jun 06 14:27:10 2018 +0100
@@ -44,7 +44,7 @@
lemma sorted_from_Suc2:
"\<lbrakk> cols xss n; i < n;
sorted_col i xss;
- \<And>x. sorted_from (i+1) (filter (\<lambda>ys. ys!i = x) xss) \<rbrakk>
+ \<And>x. sorted_from (i+1) [ys \<leftarrow> xss. ys!i = x] \<rbrakk>
\<Longrightarrow> sorted_from i xss"
proof(induction xss rule: induct_list012)
case 1 show ?case by simp
@@ -68,7 +68,7 @@
proof(rule "3.IH"[OF _ "3.prems"(2)])
show "cols (xs2 # xss) n" using "3.prems"(1) by(simp add: cols_def)
show "sorted_col i (xs2 # xss)" using "3.prems"(3) by simp
- show "\<And>x. sorted_from (i+1) (filter (\<lambda>ys. ys ! i = x) (xs2 # xss))"
+ show "\<And>x. sorted_from (i+1) [ys\<leftarrow>xs2 # xss . ys ! i = x]"
using "3.prems"(4)
sorted_antimono_suffix[OF map_mono_suffix[OF filter_mono_suffix[OF suffix_ConsI[OF suffix_order.order.refl]]]]
by fastforce
@@ -81,7 +81,7 @@
shows "sorted_from i (sort_col i xss)"
proof (rule sorted_from_Suc2[OF cols_sort1[OF assms(1)] assms(2)])
show "sorted_col i (sort_col i xss)" by(simp add: sorted)
- fix x show "sorted_from (i+1) (filter (\<lambda>ys. ys ! i = x) (sort_col i xss))"
+ fix x show "sorted_from (i+1) [ys \<leftarrow> sort_col i xss . ys ! i = x]"
proof -
from assms(3)
have "sorted_from (i+1) (filter (\<lambda>ys. ys!i = x) xss)"
--- a/src/Pure/Admin/isabelle_cronjob.scala Wed Jun 06 14:25:53 2018 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Wed Jun 06 14:27:10 2018 +0100
@@ -252,7 +252,6 @@
Remote_Build("Mac OS X 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a",
detect = Build_Log.Prop.build_start + " < date '2017-03-03'"))
-
val remote_builds1: List[List[Remote_Build]] =
{
List(
@@ -260,6 +259,12 @@
options = "-m32 -B -M1x2,2", args = "-N -g timing")),
List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90,
options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
+ List(Remote_Build("Linux Benchmarks", "lxbroy5", historic = true, history = 90,
+ options = "-m32 -B -M1x2,2 -t Benchmarks" +
+ " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
+ " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_SMLNJ=sml -e ISABELLE_SWIPL=swipl",
+ args = "-N -a -d '~~/src/Benchmarks'",
+ detect = Build_Log.Prop.build_tags + " = " + SQL.string("Benchmarks"))),
List(
Remote_Build("Mac OS X", "macbroy2",
options = "-m32 -M8" +
--- a/src/Pure/General/cache.scala Wed Jun 06 14:25:53 2018 +0100
+++ b/src/Pure/General/cache.scala Wed Jun 06 14:27:10 2018 +0100
@@ -1,4 +1,4 @@
-/* Title: Pure/cache.scala
+/* Title: Pure/General/cache.scala
Author: Makarius
cache for partial sharing (weak table).
--- a/src/Tools/jEdit/src-base/Isabelle_Base.props Wed Jun 06 14:25:53 2018 +0100
+++ b/src/Tools/jEdit/src-base/Isabelle_Base.props Wed Jun 06 14:27:10 2018 +0100
@@ -14,4 +14,4 @@
#dependencies
plugin.isabelle.jedit_base.Plugin.depend.0=jdk 1.8
-plugin.isabelle.jedit_base.Plugin.depend.1=jedit 05.04.00.00
+plugin.isabelle.jedit_base.Plugin.depend.1=jedit 05.05.00.00
--- a/src/Tools/jEdit/src/Isabelle.props Wed Jun 06 14:25:53 2018 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props Wed Jun 06 14:27:10 2018 +0100
@@ -5,7 +5,7 @@
#identification
plugin.isabelle.jedit.Plugin.name=Isabelle
plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Lars Hupel, Fabian Immler, Markus Kaiser, Makarius Wenzel
-plugin.isabelle.jedit.Plugin.version=9.0
+plugin.isabelle.jedit.Plugin.version=10.0
plugin.isabelle.jedit.Plugin.description=Isabelle Prover IDE
#system parameters
@@ -14,7 +14,7 @@
#dependencies
plugin.isabelle.jedit.Plugin.depend.0=jdk 1.8
-plugin.isabelle.jedit.Plugin.depend.1=jedit 05.04.00.00
+plugin.isabelle.jedit.Plugin.depend.1=jedit 05.05.00.00
plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 5.1.4
plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.3
plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.8