merged -- with manual conflict resolution for src/HOL/SMT_Examples/SMT_Examples.certs2, src/HOL/SMT_Examples/SMT_Word_Examples.certs2, src/Doc/Prog_Prove/document/intro-isabelle.tex;
authorwenzelm
Sun Aug 10 14:34:43 2014 +0200 (2014-08-10)
changeset 5788238bf4de248a6
parent 57881 37920df63ab9
parent 57880 47c092fd4b45
child 57883 d50aeb916a4b
merged -- with manual conflict resolution for src/HOL/SMT_Examples/SMT_Examples.certs2, src/HOL/SMT_Examples/SMT_Word_Examples.certs2, src/Doc/Prog_Prove/document/intro-isabelle.tex;
CONTRIBUTORS
NEWS
src/Doc/Prog_Prove/document/intro-isabelle.tex
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/.hgtags	Sun Aug 10 14:31:06 2014 +0200
     1.2 +++ b/.hgtags	Sun Aug 10 14:34:43 2014 +0200
     1.3 @@ -29,3 +29,6 @@
     1.4  9c1f2136532626c7cb5fae14a2aeac53be3aeb67 Isabelle2013-1
     1.5  4dd08fe126bad63aa05741d55fb3e86a2dbfc795 Isabelle2013-2
     1.6  251ef0202e719c824fe302d80a136dec025cf142 Isabelle2014-RC0
     1.7 +c0fd03d13d28954f6b7018f273b6edb17fcdeaf7 Isabelle2014-RC1
     1.8 +ee908fccabc220a5f2e5af533d13ebceeb0e09ff Isabelle2014-RC2
     1.9 +91e188508bc9df5de2737325c390836603a3e409 Isabelle2014-RC3
     2.1 --- a/Admin/Release/CHECKLIST	Sun Aug 10 14:31:06 2014 +0200
     2.2 +++ b/Admin/Release/CHECKLIST	Sun Aug 10 14:34:43 2014 +0200
     2.3 @@ -15,8 +15,6 @@
     2.4  
     2.5  - test "#!/usr/bin/env isabelle_scala_script";
     2.6  
     2.7 -- check HTML header of library;
     2.8 -
     2.9  - check sources:
    2.10      isabelle java isabelle.Check_Source '~~' '$AFP_BASE'
    2.11  
    2.12 @@ -40,6 +38,8 @@
    2.13      ROOTS
    2.14      lib/html/library_index_content.template
    2.15  
    2.16 +- check HTML header of library;
    2.17 +
    2.18  - test separate compilation of Isabelle/Scala PIDE sources:
    2.19      Admin/build jars_test
    2.20  
    2.21 @@ -54,6 +54,8 @@
    2.22  
    2.23  - Mac OS X: check app bundle with Retina display;
    2.24  
    2.25 +- Windows: check dpi scaling with high-definition display;
    2.26 +
    2.27  
    2.28  Repository fork
    2.29  ===============
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/Admin/Windows/WinRun4J/manifest.xml	Sun Aug 10 14:34:43 2014 +0200
     3.3 @@ -0,0 +1,9 @@
     3.4 +<?xml version="1.0" encoding="UTF-8" standalone="yes"?>
     3.5 +<assembly xmlns="urn:schemas-microsoft-com:asm.v1" manifestVersion="1.0" xmlns:asmv3="urn:schemas-microsoft-com:asm.v3" >
     3.6 + <asmv3:application>
     3.7 +   <asmv3:windowsSettings xmlns="http://schemas.microsoft.com/SMI/2005/WindowsSettings">
     3.8 +    <dpiAware>true</dpiAware>
     3.9 +   </asmv3:windowsSettings>
    3.10 + </asmv3:application>
    3.11 +</assembly>
    3.12 +
     4.1 --- a/Admin/components/components.sha1	Sun Aug 10 14:31:06 2014 +0200
     4.2 +++ b/Admin/components/components.sha1	Sun Aug 10 14:34:43 2014 +0200
     4.3 @@ -19,6 +19,7 @@
     4.4  e6aada354da11e533af2dee3dcdd96c06479b053  exec_process-1.0.3.tar.gz
     4.5  ae7ee5becb26512f18c609e83b34612918bae5f0  exec_process-1.0.tar.gz
     4.6  59a71e08c34ff01f3f5c4af00db5e16369527eb7  Haskabelle-2013.tar.gz
     4.7 +23a96ff4951d72f4024b6e8843262eda988bc151  Haskabelle-2014.tar.gz
     4.8  683acd94761ef460cca1a628f650355370de5afb  hol-light-bundle-0.5-126.tar.gz
     4.9  8d83e433c1419e0c0cc5fd1762903d11b4a5752c  jdk-6u31.tar.gz
    4.10  38d2d2a91c66714c18430e136e7e5191af3996e6  jdk-7u11.tar.gz
     5.1 --- a/Admin/components/main	Sun Aug 10 14:31:06 2014 +0200
     5.2 +++ b/Admin/components/main	Sun Aug 10 14:34:43 2014 +0200
     5.3 @@ -2,7 +2,7 @@
     5.4  cvc3-2.4.1
     5.5  e-1.8
     5.6  exec_process-1.0.3
     5.7 -Haskabelle-2013
     5.8 +Haskabelle-2014
     5.9  jdk-7u65
    5.10  jedit_build-20140722
    5.11  jfreechart-1.0.14-1
     6.1 --- a/Admin/lib/Tools/makedist_bundle	Sun Aug 10 14:31:06 2014 +0200
     6.2 +++ b/Admin/lib/Tools/makedist_bundle	Sun Aug 10 14:34:43 2014 +0200
     6.3 @@ -212,6 +212,7 @@
     6.4      ) > "$ISABELLE_TARGET/${ISABELLE_NAME}.ini"
     6.5  
     6.6      cp "$TMP/windows_app/Isabelle.exe" "$ISABELLE_TARGET/${ISABELLE_NAME}.exe"
     6.7 +    cp "$ISABELLE_HOME/Admin/Windows/WinRun4J/manifest.xml" "$ISABELLE_TARGET/${ISABELLE_NAME}.exe.manifest"
     6.8      cp "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Setup.bat" \
     6.9        "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Terminal.bat" "$ISABELLE_TARGET"
    6.10  
     7.1 --- a/Admin/user-aliases	Sun Aug 10 14:31:06 2014 +0200
     7.2 +++ b/Admin/user-aliases	Sun Aug 10 14:34:43 2014 +0200
     7.3 @@ -12,6 +12,7 @@
     7.4  kaliszyk@in.tum.de kaliszyk
     7.5  Philipp\ Meyer meyerp
     7.6  noschinl@in.tum.de noschinl
     7.7 +Lars Noschinski\ <noschinl@in.tum.de> noschinl
     7.8  brianh@cs.pdx.edu huffman
     7.9  nik sultana
    7.10  griff Christian Sternagel
     8.1 --- a/CONTRIBUTORS	Sun Aug 10 14:31:06 2014 +0200
     8.2 +++ b/CONTRIBUTORS	Sun Aug 10 14:34:43 2014 +0200
     8.3 @@ -19,13 +19,13 @@
     8.4    semigroups and monoids, particularly products (resp. sums) on
     8.5    finite sets.
     8.6  
     8.7 -* June 2014: Florian Haftmann, TUM
     8.8 -  Internal reorganisation of the local theory / named target stack.
     8.9 -
    8.10  * Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM
    8.11    Work on exotic automatic theorem provers for Sledgehammer (LEO-II,
    8.12    veriT, Waldmeister, etc.).
    8.13  
    8.14 +* June 2014: Florian Haftmann, TUM
    8.15 +  Internal reorganisation of the local theory / named target stack.
    8.16 +
    8.17  * June 2014: Sudeep Kanav, TUM, Jeremy Avigad, CMU, and Johannes Hölzl, TUM
    8.18    Various properties of exponentially, Erlang, and normal distributed
    8.19    random variables.
    8.20 @@ -44,6 +44,9 @@
    8.21  * Spring 2014: Lawrence C Paulson, Cambridge
    8.22    Theory Complex_Basic_Analysis. Tidying up Number_Theory vs Old_Number_Theory
    8.23  
    8.24 +* Winter 2013 and Spring 2014: Ondrej Kuncar, TUM
    8.25 +  Various improvements to Lifting/Transfer, integration with the BNF package.
    8.26 +
    8.27  * Winter 2013 and Spring 2014: Makarius Wenzel, Université Paris-Sud / LRI
    8.28    Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
    8.29  
     9.1 --- a/NEWS	Sun Aug 10 14:31:06 2014 +0200
     9.2 +++ b/NEWS	Sun Aug 10 14:34:43 2014 +0200
     9.3 @@ -97,6 +97,9 @@
     9.4  handling and propagation to enclosing text area -- avoid loosing
     9.5  keystrokes with slow / remote graphics displays.
     9.6  
     9.7 +* Completion popup supports both ENTER and TAB (default) to select an
     9.8 +item, depending on Isabelle options.
     9.9 +
    9.10  * Refined insertion of completion items wrt. jEdit text: multiple
    9.11  selections, rectangular selections, rectangular selection as "tall
    9.12  caret".
    9.13 @@ -120,6 +123,11 @@
    9.14  * More support for remote files (e.g. http) using standard Java
    9.15  networking operations instead of jEdit virtual file-systems.
    9.16  
    9.17 +* Empty editors buffers that are no longer required (e.g.\ via theory
    9.18 +imports) are automatically removed from the document model.
    9.19 +
    9.20 +* Improved monitor panel.
    9.21 +
    9.22  * Improved Console/Scala plugin: more uniform scala.Console output,
    9.23  more robust treatment of threads and interrupts.
    9.24  
    9.25 @@ -357,6 +365,42 @@
    9.26  
    9.27  INCOMPATIBILITY.
    9.28  
    9.29 +* Lifting and Transfer:
    9.30 +  - a type variable as a raw type is supported
    9.31 +  - stronger reflexivity prover
    9.32 +  - rep_eq is always generated by lift_definition
    9.33 +  - setup for Lifting/Transfer is now automated for BNFs
    9.34 +    + holds for BNFs that do not contain a dead variable
    9.35 +    + relator_eq, relator_mono, relator_distr, relator_domain,
    9.36 +      relator_eq_onp, quot_map, transfer rules for bi_unique, bi_total,
    9.37 +      right_unique, right_total, left_unique, left_total are proved
    9.38 +      automatically
    9.39 +    + definition of a predicator is generated automatically
    9.40 +    + simplification rules for a predicator definition are proved
    9.41 +      automatically for datatypes
    9.42 +  - consolidation of the setup of Lifting/Transfer
    9.43 +    + property that a relator preservers reflexivity is not needed any
    9.44 +      more
    9.45 +      Minor INCOMPATIBILITY.
    9.46 +    + left_total and left_unique rules are now transfer rules
    9.47 +      (reflexivity_rule attribute not needed anymore)
    9.48 +      INCOMPATIBILITY.
    9.49 +    + Domainp does not have to be a separate assumption in
    9.50 +      relator_domain theorems (=> more natural statement)
    9.51 +      INCOMPATIBILITY.
    9.52 +  - registration of code equations is more robust
    9.53 +    Potential INCOMPATIBILITY.
    9.54 +  - respectfulness proof obligation is preprocessed to a more readable
    9.55 +    form
    9.56 +    Potential INCOMPATIBILITY.
    9.57 +  - eq_onp is always unfolded in respectfulness proof obligation
    9.58 +    Potential INCOMPATIBILITY.
    9.59 +  - unregister lifting setup for Code_Numeral.integer and
    9.60 +    Code_Numeral.natural
    9.61 +    Potential INCOMPATIBILITY.
    9.62 +  - Lifting.invariant -> eq_onp
    9.63 +    INCOMPATIBILITY.
    9.64 +
    9.65  * New internal SAT solver "cdclite" that produces models and proof
    9.66  traces.  This solver replaces the internal SAT solvers "enumerate" and
    9.67  "dpll".  Applications that explicitly used one of these two SAT
    9.68 @@ -776,6 +820,9 @@
    9.69  * HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it
    9.70  is subsumed by session Kleene_Algebra in AFP.
    9.71  
    9.72 +* HOL-Library / theory RBT: various constants and facts are hidden;
    9.73 +lifting setup is unregistered.  INCOMPATIBILITY.
    9.74 +
    9.75  * HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.
    9.76  
    9.77  * HOL-Word: bit representations prefer type bool over type bit.
    9.78 @@ -868,6 +915,13 @@
    9.79      bounded_linear_imp_linear ~>  bounded_linear.linear
    9.80  
    9.81  * HOL-Probability:
    9.82 +  - Renamed positive_integral to nn_integral:
    9.83 +
    9.84 +    . Renamed all lemmas "*positive_integral*" to *nn_integral*"
    9.85 +      positive_integral_positive ~> nn_integral_nonneg
    9.86 +
    9.87 +    . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
    9.88 +
    9.89    - replaced the Lebesgue integral on real numbers by the more general
    9.90      Bochner integral for functions into a real-normed vector space.
    9.91  
    9.92 @@ -882,14 +936,14 @@
    9.93      integrable_nonneg           ~>  integrableI_nonneg
    9.94      integral_positive           ~>  integral_nonneg_AE
    9.95      integrable_abs_iff          ~>  integrable_abs_cancel
    9.96 -    positive_integral_lim_INF   ~>  positive_integral_liminf
    9.97 +    positive_integral_lim_INF   ~>  nn_integral_liminf
    9.98      lebesgue_real_affine        ~>  lborel_real_affine
    9.99      borel_integral_has_integral ~>  has_integral_lebesgue_integral
   9.100      integral_indicator          ~>
   9.101           integral_real_indicator / integrable_real_indicator
   9.102 -    positive_integral_fst       ~>  positive_integral_fst'
   9.103 -    positive_integral_fst_measurable ~> positive_integral_fst
   9.104 -    positive_integral_snd_measurable ~> positive_integral_snd
   9.105 +    positive_integral_fst       ~>  nn_integral_fst'
   9.106 +    positive_integral_fst_measurable ~> nn_integral_fst
   9.107 +    positive_integral_snd_measurable ~> nn_integral_snd
   9.108  
   9.109      integrable_fst_measurable   ~>
   9.110           integral_fst / integrable_fst / AE_integrable_fst
   9.111 @@ -915,7 +969,7 @@
   9.112           integrable_has_integral_lebesgue_nonneg
   9.113  
   9.114      lebesgue_integral_real_affine  ~>
   9.115 -         positive_integral_real_affine
   9.116 +         nn_integral_real_affine
   9.117  
   9.118      has_integral_iff_positive_integral_lborel  ~>
   9.119           integral_has_integral_nonneg / integrable_has_integral_nonneg
   9.120 @@ -930,13 +984,6 @@
   9.121      integral_cmul_indicator
   9.122      integral_real
   9.123  
   9.124 -  - Renamed positive_integral to nn_integral:
   9.125 -
   9.126 -    . Renamed all lemmas "*positive_integral*" to *nn_integral*"
   9.127 -      positive_integral_positive ~> nn_integral_nonneg
   9.128 -
   9.129 -    . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
   9.130 -
   9.131    - Formalized properties about exponentially, Erlang, and normal
   9.132      distributed random variables.
   9.133  
    10.1 --- a/etc/options	Sun Aug 10 14:31:06 2014 +0200
    10.2 +++ b/etc/options	Sun Aug 10 14:34:43 2014 +0200
    10.3 @@ -117,6 +117,9 @@
    10.4  public option editor_output_delay : real = 0.1
    10.5    -- "delay for prover output (markup, common messages etc.)"
    10.6  
    10.7 +public option editor_prune_delay : real = 60.0
    10.8 +  -- "delay to prune history (delete old versions)"
    10.9 +
   10.10  public option editor_update_delay : real = 0.5
   10.11    -- "delay for physical GUI updates"
   10.12  
    11.1 --- a/src/Doc/Implementation/ML.thy	Sun Aug 10 14:31:06 2014 +0200
    11.2 +++ b/src/Doc/Implementation/ML.thy	Sun Aug 10 14:34:43 2014 +0200
    11.3 @@ -722,9 +722,10 @@
    11.4  
    11.5    \begin{description}
    11.6  
    11.7 -  \item @{text "@{make_string}"} inlines a function to print arbitrary
    11.8 -  values similar to the ML toplevel.  The result is compiler dependent
    11.9 -  and may fall back on "?" in certain situations.
   11.10 +  \item @{text "@{make_string}"} inlines a function to print arbitrary values
   11.11 +  similar to the ML toplevel. The result is compiler dependent and may fall
   11.12 +  back on "?" in certain situations. The value of configuration option
   11.13 +  @{attribute_ref ML_print_depth} determines further details of output.
   11.14  
   11.15    \item @{text "@{print f}"} uses the ML function @{text "f: string ->
   11.16    unit"} to output the result of @{text "@{make_string}"} above,
    12.1 --- a/src/Doc/Implementation/Syntax.thy	Sun Aug 10 14:31:06 2014 +0200
    12.2 +++ b/src/Doc/Implementation/Syntax.thy	Sun Aug 10 14:34:43 2014 +0200
    12.3 @@ -99,7 +99,7 @@
    12.4    If particular type-constraints are required for some of the arguments, the
    12.5    read operations needs to be split into its parse and check phases. Then it
    12.6    is possible to use @{ML Type.constraint} on the intermediate pre-terms
    12.7 -  \secref{sec:term-check}.
    12.8 +  (\secref{sec:term-check}).
    12.9  
   12.10    \item @{ML Syntax.read_props}~@{text "ctxt strs"} parses and checks a
   12.11    simultaneous list of source strings as terms of the logic, with an implicit
    13.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Aug 10 14:31:06 2014 +0200
    13.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Aug 10 14:34:43 2014 +0200
    13.3 @@ -1542,6 +1542,10 @@
    13.4      @{text "bi_unique A \<Longrightarrow> (list_all2 A ===> op =) distinct distinct"}\\
    13.5      @{text "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (rel_prod A B)"}
    13.6  
    13.7 +    Preservation of predicates on relations (@{text "bi_unique, bi_total,
    13.8 +    right_unique, right_total, left_unique, left_total"}) with the respect to a relator
    13.9 +    is proved automatically if the involved type is BNF\cite{isabelle-datatypes} without dead variables.
   13.10 +
   13.11    \item @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection
   13.12      of rules, which specify a domain of a transfer relation by a predicate.
   13.13      E.g., given the transfer relation @{text "ZN x n \<equiv> (x = int n)"}, 
   13.14 @@ -1550,15 +1554,19 @@
   13.15      more readable transferred goals, e.g., when quantifiers are transferred.
   13.16  
   13.17    \item @{attribute (HOL) relator_eq} attribute collects identity laws
   13.18 -    for relators of various type constructors, e.g. @{text "list_all2
   13.19 +    for relators of various type constructors, e.g. @{term "rel_set
   13.20      (op =) = (op =)"}. The @{method (HOL) transfer} method uses these
   13.21      lemmas to infer transfer rules for non-polymorphic constants on
   13.22 -    the fly.
   13.23 +    the fly. For examples see @{file
   13.24 +    "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. 
   13.25 +    This property is proved automatically if the involved type is BNF without dead variables.
   13.26  
   13.27    \item @{attribute_def (HOL) "relator_domain"} attribute collects rules 
   13.28 -    describing domains of relators by predicators. E.g., @{text "Domainp A = P \<Longrightarrow>
   13.29 -    Domainp (list_all2 A) = (list_all P)"}. This allows the package to lift transfer
   13.30 -    domain rules through type constructors.
   13.31 +    describing domains of relators by predicators. E.g., 
   13.32 +    @{term "Domainp (rel_set T) = (\<lambda>A. Ball A (Domainp T))"}. This allows the package 
   13.33 +    to lift transfer domain rules through type constructors. For examples see @{file
   13.34 +    "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
   13.35 +    This property is proved automatically if the involved type is BNF without dead variables.
   13.36  
   13.37    \end{description}
   13.38  
   13.39 @@ -1603,7 +1611,7 @@
   13.40  
   13.41    @{rail \<open>
   13.42      @@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type}  @{syntax mixfix}? \<newline>
   13.43 -      'is' @{syntax term} (@'parametric' @{syntax thmref})?;
   13.44 +      'is' @{syntax term} (@'parametric' (@{syntax thmref}+))?;
   13.45    \<close>}
   13.46  
   13.47    @{rail \<open>
   13.48 @@ -1625,10 +1633,10 @@
   13.49      The command supports two modes. The first one is a low-level mode when 
   13.50      the user must provide as a first
   13.51      argument of @{command (HOL) "setup_lifting"} a
   13.52 -    quotient theorem @{text "Quotient R Abs Rep T"}. The
   13.53 +    quotient theorem @{term "Quotient R Abs Rep T"}. The
   13.54      package configures a transfer rule for equality, a domain transfer
   13.55      rules and sets up the @{command_def (HOL) "lift_definition"}
   13.56 -    command to work with the abstract type. An optional theorem @{text "reflp R"}, which certifies that 
   13.57 +    command to work with the abstract type. An optional theorem @{term "reflp R"}, which certifies that 
   13.58      the equivalence relation R is total,
   13.59      can be provided as a second argument. This allows the package to generate stronger transfer
   13.60      rules. And finally, the parametricity theorem for R can be provided as a third argument.
   13.61 @@ -1671,9 +1679,9 @@
   13.62      @{text f.transfer} for the Transfer package are generated by the
   13.63      package.
   13.64  
   13.65 -    The user can specify a parametricity theorem for @{text t} after the keyword 
   13.66 +    The user can specify a parametricity theorems for @{text t} after the keyword 
   13.67      @{keyword "parametric"}, which allows the command
   13.68 -    to generate a parametric transfer rule for @{text f}.
   13.69 +    to generate parametric transfer rules for @{text f}.
   13.70  
   13.71      For each constant defined through trivial quotients (type copies or
   13.72      subtypes) @{text f.rep_eq} is generated. The equation is a code certificate
   13.73 @@ -1720,38 +1728,42 @@
   13.74      theorems.
   13.75  
   13.76    \item @{attribute (HOL) quot_map} registers a quotient map
   13.77 -    theorem. E.g., @{text "Quotient R Abs Rep T \<Longrightarrow> 
   13.78 -    Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)"}. 
   13.79 +    theorem, a theorem showing how to "lift" quotients over type constructors. 
   13.80 +    E.g., @{term "Quotient R Abs Rep T \<Longrightarrow> 
   13.81 +    Quotient (rel_set R) (image Abs) (image Rep) (rel_set T)"}. 
   13.82      For examples see @{file
   13.83 -    "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files
   13.84 -    in the same directory.
   13.85 +    "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
   13.86 +    This property is proved automatically if the involved type is BNF without dead variables.
   13.87  
   13.88    \item @{attribute (HOL) relator_eq_onp} registers a theorem that
   13.89 -    shows a relationship between the constant @{text
   13.90 -    eq_onp} (used for internal encoding of proper subtypes)
   13.91 -    and a relator.  Such theorems allows the package to hide @{text
   13.92 +    shows that a relator applied to an equality restricted by a predicate @{term P} (i.e., @{term
   13.93 +    "eq_onp P"}) is equal 
   13.94 +    to a predicator applied to the @{term P}. The combinator @{const eq_onp} is used for 
   13.95 +    internal encoding of proper subtypes. Such theorems allows the package to hide @{text
   13.96      eq_onp} from a user in a user-readable form of a
   13.97      respectfulness theorem. For examples see @{file
   13.98 -    "~~/src/HOL/List.thy"} or Lifting_*.thy files in the same directory.
   13.99 +    "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
  13.100 +    This property is proved automatically if the involved type is BNF without dead variables.
  13.101  
  13.102    \item @{attribute (HOL) "relator_mono"} registers a property describing a monotonicity of a relator.
  13.103 -    E.g., @{text "A \<le> B \<Longrightarrow> list_all2 A \<le> list_all2 B"}. For examples 
  13.104 -    see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} 
  13.105 -    or Lifting_*.thy files in the same directory.
  13.106 +    E.g., @{term "A \<le> B \<Longrightarrow> rel_set A \<le> rel_set B"}. 
  13.107      This property is needed for proving a stronger transfer rule in @{command_def (HOL) "lift_definition"}
  13.108 -    when a parametricity theorem for the raw term is specified.
  13.109 +    when a parametricity theorem for the raw term is specified and also for the reflexivity prover.
  13.110 +    For examples see @{file
  13.111 +    "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
  13.112 +    This property is proved automatically if the involved type is BNF without dead variables.
  13.113  
  13.114    \item @{attribute (HOL) "relator_distr"} registers a property describing a distributivity
  13.115      of the relation composition and a relator. E.g., 
  13.116 -    @{text "list_all2 R \<circ>\<circ> list_all2 S = list_all2 (R \<circ>\<circ> S)"}. 
  13.117 +    @{text "rel_set R \<circ>\<circ> rel_set S = rel_set (R \<circ>\<circ> S)"}. 
  13.118      This property is needed for proving a stronger transfer rule in @{command_def (HOL) "lift_definition"}
  13.119      when a parametricity theorem for the raw term is specified.
  13.120      When this equality does not hold unconditionally (e.g., for the function type), the user can specified
  13.121      each direction separately and also register multiple theorems with different set of assumptions.
  13.122      This attribute can be used only after the monotonicity property was already registered by
  13.123 -    @{attribute (HOL) "relator_mono"}. For examples 
  13.124 -    see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} 
  13.125 -    or Lifting_*.thy files in the same directory.
  13.126 +    @{attribute (HOL) "relator_mono"}. For examples see @{file
  13.127 +    "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
  13.128 +    This property is proved automatically if the involved type is BNF without dead variables.
  13.129  
  13.130    \item @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem
  13.131      from the Lifting infrastructure and thus de-register the corresponding quotient. 
  13.132 @@ -1773,6 +1785,14 @@
  13.133      together with the commands @{command (HOL) lifting_forget} and @{command (HOL) lifting_update} is
  13.134      preferred for normal usage.
  13.135  
  13.136 +  \item Integration with the BNF package\cite{isabelle-datatypes}: 
  13.137 +    As already mentioned, the theorems that are registered
  13.138 +    by the following attributes are proved and registered automatically if the involved type
  13.139 +    is BNF without dead variables: @{attribute (HOL) quot_map}, @{attribute (HOL) relator_eq_onp}, 
  13.140 +    @{attribute (HOL) "relator_mono"}, @{attribute (HOL) "relator_distr"}. Also the definition of a 
  13.141 +    relator and predicator is provided automatically. Moreover, if the BNF represents a datatype, 
  13.142 +    simplification rules for a predicator are again proved automatically.
  13.143 +  
  13.144    \end{description}
  13.145  *}
  13.146  
    14.1 --- a/src/Doc/JEdit/JEdit.thy	Sun Aug 10 14:31:06 2014 +0200
    14.2 +++ b/src/Doc/JEdit/JEdit.thy	Sun Aug 10 14:34:43 2014 +0200
    14.3 @@ -1298,20 +1298,21 @@
    14.4    A \emph{completion popup} is a minimally invasive GUI component over the
    14.5    text area that offers a selection of completion items to be inserted into
    14.6    the text, e.g.\ by mouse clicks. Items are sorted dynamically, according to
    14.7 -  the frequency of selection, with persistent history. The popup interprets
    14.8 -  special keys @{verbatim TAB}, @{verbatim ESCAPE}, @{verbatim UP}, @{verbatim
    14.9 -  DOWN}, @{verbatim PAGE_UP}, @{verbatim PAGE_DOWN}, but all other key events
   14.10 -  are passed to the underlying text area. This allows to ignore unwanted
   14.11 -  completions most of the time and continue typing quickly. Thus the popup
   14.12 -  serves as a mechanism of confirmation of proposed items, but the default is
   14.13 -  to continue without completion.
   14.14 +  the frequency of selection, with persistent history. The popup may interpret
   14.15 +  special keys @{verbatim ENTER}, @{verbatim TAB}, @{verbatim ESCAPE},
   14.16 +  @{verbatim UP}, @{verbatim DOWN}, @{verbatim PAGE_UP}, @{verbatim
   14.17 +  PAGE_DOWN}, but all other key events are passed to the underlying text area.
   14.18 +  This allows to ignore unwanted completions most of the time and continue
   14.19 +  typing quickly. Thus the popup serves as a mechanism of confirmation of
   14.20 +  proposed items, but the default is to continue without completion.
   14.21  
   14.22    The meaning of special keys is as follows:
   14.23  
   14.24    \medskip
   14.25    \begin{tabular}{ll}
   14.26    \textbf{key} & \textbf{action} \\\hline
   14.27 -  @{verbatim "TAB"} & select completion \\
   14.28 +  @{verbatim "ENTER"} & select completion (if @{system_option jedit_completion_select_enter}) \\
   14.29 +  @{verbatim "TAB"} & select completion (if @{system_option jedit_completion_select_tab}) \\
   14.30    @{verbatim "ESCAPE"} & dismiss popup \\
   14.31    @{verbatim "UP"} & move up one item \\
   14.32    @{verbatim "DOWN"} & move down one item \\
   14.33 @@ -1385,6 +1386,11 @@
   14.34    regular jEdit key events (\secref{sec:completion-input}): it allows to
   14.35    disable implicit completion altogether.
   14.36  
   14.37 +  \item @{system_option_def jedit_completion_select_enter} and
   14.38 +  @{system_option_def jedit_completion_select_tab} enable keys to select a
   14.39 +  completion item from the popup (\secref{sec:completion-popup}). Note that a
   14.40 +  regular mouse click on the list of items is always possible.
   14.41 +
   14.42    \item @{system_option_def jedit_completion_context} specifies whether the
   14.43    language context provided by the prover should be used at all. Disabling
   14.44    that option makes completion less ``semantic''. Note that incomplete or
   14.45 @@ -1589,14 +1595,14 @@
   14.46    @{system_option_ref jedit_timing_threshold}, which can be configured in
   14.47    \emph{Plugin Options~/ Isabelle~/ General}.
   14.48  
   14.49 -  \medskip The \emph{Monitor} panel provides a general impression of
   14.50 -  recent activity of the farm of worker threads in Isabelle/ML.  Its
   14.51 -  display is continuously updated according to @{system_option_ref
   14.52 -  editor_chart_delay}.  Note that the painting of the chart takes
   14.53 -  considerable runtime itself --- on the Java Virtual Machine that
   14.54 -  runs Isabelle/Scala, not Isabelle/ML.  Internally, the
   14.55 -  Isabelle/Scala module @{verbatim isabelle.ML_Statistics} provides
   14.56 -  further access to statistics of Isabelle/ML.  *}
   14.57 +  \medskip The \emph{Monitor} panel visualizes various data collections about
   14.58 +  recent activity of the Isabelle/ML task farm and the underlying ML runtime
   14.59 +  system. The display is continuously updated according to @{system_option_ref
   14.60 +  editor_chart_delay}. Note that the painting of the chart takes considerable
   14.61 +  runtime itself --- on the Java Virtual Machine that runs Isabelle/Scala, not
   14.62 +  Isabelle/ML. Internally, the Isabelle/Scala module @{verbatim
   14.63 +  isabelle.ML_Statistics} provides further access to statistics of
   14.64 +  Isabelle/ML. *}
   14.65  
   14.66  
   14.67  section {* Low-level output *}
   14.68 @@ -1662,11 +1668,11 @@
   14.69    \textbf{Workaround:} Copy/paste complete command text from
   14.70    elsewhere, or disable continuous checking temporarily.
   14.71  
   14.72 -  \item \textbf{Problem:} No way to delete document nodes from the overall
   14.73 +  \item \textbf{Problem:} No direct support to remove document nodes from the
   14.74    collection of theories.
   14.75  
   14.76 -  \textbf{Workaround:} Ignore unused files.  Restart whole
   14.77 -  Isabelle/jEdit session in worst-case situation.
   14.78 +  \textbf{Workaround:} Clear the buffer content of unused files and close
   14.79 +  \emph{without} saving changes.
   14.80  
   14.81    \item \textbf{Problem:} Keyboard shortcuts @{verbatim "C+PLUS"} and
   14.82    @{verbatim "C+MINUS"} for adjusting the editor font size depend on
    15.1 --- a/src/Doc/Prog_Prove/document/root.bib	Sun Aug 10 14:31:06 2014 +0200
    15.2 +++ b/src/Doc/Prog_Prove/document/root.bib	Sun Aug 10 14:34:43 2014 +0200
    15.3 @@ -18,7 +18,7 @@
    15.4  
    15.5  @book{ConcreteSemantics,author={Tobias Nipkow and Gerwin Klein},
    15.6  title="Concrete Semantics. A Proof Assistant Approach",
    15.7 -publisher={\url{http://www.in.tum.de/~nipkow/Concrete}},year=2013}
    15.8 +publisher={\url{http://www.concrete-semantics.org}},year=2013}
    15.9  
   15.10  @manual{IsarRef,author={Makarius Wenzel},
   15.11  title={The Isabelle/Isar Reference Manual},
    16.1 --- a/src/Doc/System/Scala.thy	Sun Aug 10 14:31:06 2014 +0200
    16.2 +++ b/src/Doc/System/Scala.thy	Sun Aug 10 14:34:43 2014 +0200
    16.3 @@ -61,7 +61,7 @@
    16.4  
    16.5    This allows to compile further Scala modules, depending on existing
    16.6    Isabelle/Scala functionality.  The resulting class or jar files can
    16.7 -  be added to the Java classpath the @{verbatim classpath} Bash
    16.8 +  be added to the Java classpath using the @{verbatim classpath} Bash
    16.9    function that is provided by the Isabelle process environment.  Thus
   16.10    add-on components can register themselves in a modular manner, see
   16.11    also \secref{sec:components}.
    17.1 --- a/src/Doc/manual.bib	Sun Aug 10 14:31:06 2014 +0200
    17.2 +++ b/src/Doc/manual.bib	Sun Aug 10 14:34:43 2014 +0200
    17.3 @@ -351,6 +351,12 @@
    17.4    pages = "93--110"
    17.5  }
    17.6  
    17.7 +@manual{isabelle-datatypes,
    17.8 +  author	= {Jasmin Christian Blanchette and Martin Desharnais and Lorenz Panny and Andrei Popescu and Dmitriy Traytel},
    17.9 +  title		= {Defining (Co)datatypes in Isabelle/HOL},
   17.10 +  institution	= {TU Munich},
   17.11 +  note          = {\url{http://isabelle.in.tum.de/doc/datatypes.pdf}}}
   17.12 +
   17.13  @inproceedings{why3,
   17.14    author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
   17.15    title = {{Why3}: Shepherd Your Herd of Provers},
    18.1 --- a/src/HOL/Algebra/Divisibility.thy	Sun Aug 10 14:31:06 2014 +0200
    18.2 +++ b/src/HOL/Algebra/Divisibility.thy	Sun Aug 10 14:34:43 2014 +0200
    18.3 @@ -74,7 +74,7 @@
    18.4    have c: "inv (a \<otimes> b) \<otimes> a \<in> carrier G" by simp
    18.5  
    18.6    have "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = inv (a \<otimes> b) \<otimes> (a \<otimes> b)" by (simp add: m_assoc)
    18.7 -  also have "\<dots> = \<one>" by (simp add: Units_l_inv)
    18.8 +  also have "\<dots> = \<one>" by simp
    18.9    finally have li: "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = \<one>" .
   18.10  
   18.11    have "\<one> = inv a \<otimes> a" by (simp add: Units_l_inv[symmetric])
   18.12 @@ -83,7 +83,7 @@
   18.13         by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv)
   18.14    also have "\<dots> = ((inv a \<otimes> a) \<otimes> b) \<otimes> inv (a \<otimes> b) \<otimes> a"
   18.15      by (simp add: m_assoc del: Units_l_inv)
   18.16 -  also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by (simp add: Units_l_inv)
   18.17 +  also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by simp
   18.18    also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> a)" by (simp add: m_assoc)
   18.19    finally have ri: "b \<otimes> (inv (a \<otimes> b) \<otimes> a) = \<one> " by simp
   18.20  
   18.21 @@ -327,7 +327,7 @@
   18.22  unfolding a
   18.23  apply (intro associatedI)
   18.24   apply (rule dividesI[of "inv u"], simp)
   18.25 - apply (simp add: m_assoc Units_closed Units_r_inv)
   18.26 + apply (simp add: m_assoc Units_closed)
   18.27  apply fast
   18.28  done
   18.29  
   18.30 @@ -1764,7 +1764,7 @@
   18.31    note [simp] = acarr Units_closed[OF uunit] Units_inv_closed[OF uunit]
   18.32  
   18.33    have "a = a \<otimes> \<one>" by simp
   18.34 -  also have "\<dots> = a \<otimes> (u \<otimes> inv u)" by (simp add: Units_r_inv uunit)
   18.35 +  also have "\<dots> = a \<otimes> (u \<otimes> inv u)" by (simp add: uunit)
   18.36    also have "\<dots> = a' \<otimes> inv u" by (simp add: m_assoc[symmetric] a'[symmetric])
   18.37    finally
   18.38         have a: "a = a' \<otimes> inv u" .
   18.39 @@ -2646,7 +2646,7 @@
   18.40      hence yb: "fmset G ys \<le> fmset G bs" by (rule divides_fmsubset) fact+
   18.41  
   18.42      from ya yb csmset
   18.43 -    have "fmset G ys \<le> fmset G cs" by (simp add: mset_le_def multiset_inter_count)
   18.44 +    have "fmset G ys \<le> fmset G cs" by (simp add: mset_le_def)
   18.45      thus "y divides c" by (rule fmsubset_divides) fact+
   18.46    qed
   18.47  
   18.48 @@ -3208,7 +3208,7 @@
   18.49            and nyx: "\<not> y \<sim> x"
   18.50            by - (fast elim: properfactorE2)+
   18.51        hence "\<exists>z. z \<in> carrier G \<and> x = y \<otimes> z"
   18.52 -          by (fast elim: dividesE)
   18.53 +          by fast
   18.54  
   18.55        from this obtain z
   18.56            where zcarr: "z \<in> carrier G"
   18.57 @@ -3327,7 +3327,7 @@
   18.58        and afs': "wfactors G as' a"
   18.59      hence ahdvda: "ah divides a"
   18.60        by (intro wfactors_dividesI[of "ah#as" "a"], simp+)
   18.61 -    hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by (fast elim: dividesE)
   18.62 +    hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by fast
   18.63      from this obtain a'
   18.64        where a'carr: "a' \<in> carrier G"
   18.65        and a: "a = ah \<otimes> a'"
   18.66 @@ -3360,7 +3360,7 @@
   18.67        have asicarr[simp]: "as'!i \<in> carrier G" by (unfold set_conv_nth, force)
   18.68      note carr = carr asicarr
   18.69  
   18.70 -    from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by (fast elim: dividesE)
   18.71 +    from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by fast
   18.72      from this obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" by auto
   18.73  
   18.74      with carr irrasi[simplified asi]
   18.75 @@ -3454,7 +3454,7 @@
   18.76      next
   18.77        show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'"
   18.78        apply (simp add: list_all2_append)
   18.79 -      apply (simp add: asiah[symmetric] ahcarr asicarr)
   18.80 +      apply (simp add: asiah[symmetric])
   18.81        done
   18.82      qed
   18.83  
   18.84 @@ -3463,12 +3463,12 @@
   18.85      also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
   18.86        (take i as' @ as' ! i # drop (Suc i) as')"
   18.87        apply (intro essentially_equalI)
   18.88 -      apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~> 
   18.89 +       apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~> 
   18.90          take i as' @ as' ! i # drop (Suc i) as'")
   18.91 -  apply simp
   18.92 +        apply simp
   18.93         apply (rule perm_append_Cons)
   18.94        apply simp
   18.95 -    done
   18.96 +      done
   18.97      finally
   18.98        have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')" by simp
   18.99      then show "essentially_equal G (ah # as) as'" by (subst as', assumption)
  18.100 @@ -3617,7 +3617,7 @@
  18.101      also from ccarr acarr cunit
  18.102          have "\<dots> = a \<otimes> (c \<otimes> inv c)" by (fast intro: m_assoc)
  18.103      also from ccarr cunit
  18.104 -        have "\<dots> = a \<otimes> \<one>" by (simp add: Units_r_inv)
  18.105 +        have "\<dots> = a \<otimes> \<one>" by simp
  18.106      also from acarr
  18.107          have "\<dots> = a" by simp
  18.108      finally have "a = b \<otimes> inv c" by simp
  18.109 @@ -3706,7 +3706,7 @@
  18.110    shows "(divisor_chain_condition_monoid G \<and> gcd_condition_monoid G) = factorial_monoid G"
  18.111  apply rule
  18.112  proof clarify
  18.113 -    assume dcc: "divisor_chain_condition_monoid G"
  18.114 +  assume dcc: "divisor_chain_condition_monoid G"
  18.115       and gc: "gcd_condition_monoid G"
  18.116    interpret divisor_chain_condition_monoid "G" by (rule dcc)
  18.117    interpret gcd_condition_monoid "G" by (rule gc)
    19.1 --- a/src/HOL/Algebra/Exponent.thy	Sun Aug 10 14:31:06 2014 +0200
    19.2 +++ b/src/HOL/Algebra/Exponent.thy	Sun Aug 10 14:34:43 2014 +0200
    19.3 @@ -249,7 +249,7 @@
    19.4  apply (simp (no_asm))
    19.5  (*induction step*)
    19.6  apply (subgoal_tac "(Suc (j+k) choose Suc k) > 0")
    19.7 - prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
    19.8 + prefer 2 apply (simp, clarify)
    19.9  apply (subgoal_tac "exponent p ((Suc (j+k) choose Suc k) * Suc k) = 
   19.10                      exponent p (Suc k)")
   19.11   txt{*First, use the assumed equation.  We simplify the LHS to
   19.12 @@ -260,7 +260,7 @@
   19.13     @{text Suc_times_binomial_eq} ...*}
   19.14  apply (simp del: bad_Sucs add: Suc_times_binomial_eq [symmetric])
   19.15  txt{*...then @{text exponent_mult_add} and the quantified premise.*}
   19.16 -apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add)
   19.17 +apply (simp del: bad_Sucs add: exponent_mult_add)
   19.18  done
   19.19  
   19.20  (*The lemma above, with two changes of variables*)
    20.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sun Aug 10 14:31:06 2014 +0200
    20.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Sun Aug 10 14:34:43 2014 +0200
    20.3 @@ -528,7 +528,7 @@
    20.4      case 0 with R show ?thesis by simp
    20.5    next
    20.6      case Suc with R show ?thesis
    20.7 -      using R.finsum_Suc2 by (simp del: R.finsum_Suc add: R.r_null Pi_def)
    20.8 +      using R.finsum_Suc2 by (simp del: R.finsum_Suc add: Pi_def)
    20.9    qed
   20.10  qed (simp_all add: R)
   20.11  
    21.1 --- a/src/HOL/Library/AList_Mapping.thy	Sun Aug 10 14:31:06 2014 +0200
    21.2 +++ b/src/HOL/Library/AList_Mapping.thy	Sun Aug 10 14:34:43 2014 +0200
    21.3 @@ -60,7 +60,7 @@
    21.4    have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
    21.5      by (auto simp add: image_def intro!: bexI)
    21.6    show ?thesis apply transfer
    21.7 -  by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux)
    21.8 +    by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux)
    21.9  qed
   21.10  
   21.11  lemma [code nbe]:
    22.1 --- a/src/HOL/Library/Diagonal_Subsequence.thy	Sun Aug 10 14:31:06 2014 +0200
    22.2 +++ b/src/HOL/Library/Diagonal_Subsequence.thy	Sun Aug 10 14:34:43 2014 +0200
    22.3 @@ -27,8 +27,10 @@
    22.4  
    22.5  lemma subseq_seqseq[intro, simp]: "subseq (seqseq n)"
    22.6  proof (induct n)
    22.7 -  case (Suc n) thus ?case by (subst seqseq.simps) (auto simp: subseq_reduce intro!: subseq_o)
    22.8 -qed (simp add: subseq_def)
    22.9 +  case 0 thus ?case by (simp add: subseq_def)
   22.10 +next
   22.11 +  case (Suc n) thus ?case by (subst seqseq.simps) (auto intro!: subseq_o)
   22.12 +qed
   22.13  
   22.14  lemma seqseq_holds:
   22.15    "P n (seqseq (Suc n))"
    23.1 --- a/src/HOL/Library/Float.thy	Sun Aug 10 14:31:06 2014 +0200
    23.2 +++ b/src/HOL/Library/Float.thy	Sun Aug 10 14:34:43 2014 +0200
    23.3 @@ -610,8 +610,7 @@
    23.4      by (auto intro: exI[where x="m*2^nat (e+p)"]
    23.5               simp add: ac_simps powr_add[symmetric] r powr_realpow)
    23.6    with `\<not> p + e < 0` show ?thesis
    23.7 -    by transfer
    23.8 -       (auto simp add: round_down_def field_simps powr_add powr_minus inverse_eq_divide)
    23.9 +    by transfer (auto simp add: round_down_def field_simps powr_add powr_minus)
   23.10  qed
   23.11  hide_fact (open) compute_float_down
   23.12  
   23.13 @@ -682,8 +681,7 @@
   23.14      by (auto simp add: ac_simps powr_add[symmetric] r1 powr_realpow
   23.15        intro: exI[where x="m*2^nat (e+p)"])
   23.16    then show ?thesis using `\<not> p + e < 0`
   23.17 -    by transfer
   23.18 -       (simp add: round_up_def floor_divide_eq_div field_simps powr_add powr_minus inverse_eq_divide)
   23.19 +    by transfer (simp add: round_up_def floor_divide_eq_div field_simps powr_add powr_minus)
   23.20  qed
   23.21  hide_fact (open) compute_float_up
   23.22  
   23.23 @@ -840,7 +838,7 @@
   23.24      have "(1::int) < 2" by simp
   23.25      case False let ?S = "2^(nat (-e))"
   23.26      have "inverse (2 ^ nat (- e)) = 2 powr e" using assms False powr_realpow[of 2 "nat (-e)"]
   23.27 -      by (auto simp: powr_minus field_simps inverse_eq_divide)
   23.28 +      by (auto simp: powr_minus field_simps)
   23.29      hence "1 \<le> real m * inverse ?S" using assms False powr_realpow[of 2 "nat (-e)"]
   23.30        by (auto simp: powr_minus)
   23.31      hence "1 * ?S \<le> real m * inverse ?S * ?S" by (rule mult_right_mono, auto)
   23.32 @@ -940,7 +938,7 @@
   23.33      have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult int_power)
   23.34      moreover have "real x * real (2::int) powr real l / real y = x / real y'"
   23.35        using `\<not> 0 \<le> l`
   23.36 -      by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps inverse_eq_divide)
   23.37 +      by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps)
   23.38      ultimately show ?thesis
   23.39        unfolding normfloat_def
   23.40        using ceil_divide_floor_conv[of y' x] `\<not> 0 \<le> l` `y' \<noteq> 0` `y \<noteq> 0`
   23.41 @@ -993,7 +991,7 @@
   23.42      using rat_precision_pos[OF assms] by (rule power_aux)
   23.43    finally show ?thesis
   23.44      apply (transfer fixing: n x y)
   23.45 -    apply (simp add: round_up_def field_simps powr_minus inverse_eq_divide powr1)
   23.46 +    apply (simp add: round_up_def field_simps powr_minus powr1)
   23.47      unfolding int_of_reals real_of_int_less_iff
   23.48      apply (simp add: ceiling_less_eq)
   23.49      done
   23.50 @@ -1415,7 +1413,7 @@
   23.51      by (simp add: powr_divide2[symmetric] powr_add powr_minus inverse_eq_divide)
   23.52    also have "\<dots> = 2 powr (log 2 x - (real \<lfloor>log 2 x\<rfloor>) - 1)"
   23.53      using `0 < x`
   23.54 -    by (auto simp: inverse_eq_divide field_simps powr_add powr_divide2[symmetric])
   23.55 +    by (auto simp: field_simps powr_add powr_divide2[symmetric])
   23.56    also have "\<dots> < 2 powr 0"
   23.57      using real_of_int_floor_add_one_gt
   23.58      unfolding neg_less_iff_less
    24.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun Aug 10 14:31:06 2014 +0200
    24.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun Aug 10 14:34:43 2014 +0200
    24.3 @@ -808,7 +808,7 @@
    24.4        then have tw: "cmod ?w \<le> cmod w"
    24.5          using t(1) by (simp add: norm_mult)
    24.6        from t inv0 have "t * (cmod w ^ (k + 1) * m) < 1"
    24.7 -        by (simp add: inverse_eq_divide field_simps)
    24.8 +        by (simp add: field_simps)
    24.9        with zero_less_power[OF t(1), of k] have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
   24.10          by (metis comm_mult_strict_left_mono)
   24.11        have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k + 1) * cmod (poly s ?w)))"
    25.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Sun Aug 10 14:31:06 2014 +0200
    25.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Sun Aug 10 14:34:43 2014 +0200
    25.3 @@ -396,7 +396,7 @@
    25.4    proof -
    25.5      have g: "\<bar>a\<bar> + \<bar>b\<bar> = sup (a + b) (sup (- a - b) (sup (- a + b) (a + (- b))))"
    25.6        (is "_=sup ?m ?n")
    25.7 -      by (simp add: abs_lattice add_sup_inf_distribs sup_aci ac_simps)
    25.8 +      by (simp add: abs_lattice add_sup_inf_distribs ac_simps)
    25.9      have a: "a + b \<le> sup ?m ?n"
   25.10        by simp
   25.11      have b: "- a - b \<le> ?n"
   25.12 @@ -410,7 +410,7 @@
   25.13      from a d e have "\<bar>a + b\<bar> \<le> sup ?m ?n"
   25.14        apply -
   25.15        apply (drule abs_leI)
   25.16 -      apply (simp_all only: algebra_simps ac_simps minus_add)
   25.17 +      apply (simp_all only: algebra_simps minus_add)
   25.18        apply (metis add_uminus_conv_diff d sup_commute uminus_add_conv_diff)
   25.19        done
   25.20      with g[symmetric] show ?thesis by simp
    26.1 --- a/src/HOL/Library/Polynomial.thy	Sun Aug 10 14:31:06 2014 +0200
    26.2 +++ b/src/HOL/Library/Polynomial.thy	Sun Aug 10 14:34:43 2014 +0200
    26.3 @@ -1315,8 +1315,7 @@
    26.4      then have "finite {x. poly k x = 0}" using `k \<noteq> 0` by (rule Suc.hyps)
    26.5      then have "finite (insert a {x. poly k x = 0})" by simp
    26.6      then show "finite {x. poly p x = 0}"
    26.7 -      by (simp add: k uminus_add_conv_diff Collect_disj_eq
    26.8 -               del: mult_pCons_left)
    26.9 +      by (simp add: k Collect_disj_eq del: mult_pCons_left)
   26.10    qed
   26.11  qed
   26.12  
    27.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Aug 10 14:31:06 2014 +0200
    27.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Aug 10 14:34:43 2014 +0200
    27.3 @@ -137,17 +137,17 @@
    27.4  end
    27.5  *} "lift trivial vector statements to real arith statements"
    27.6  
    27.7 -lemma vec_0[simp]: "vec 0 = 0" by (vector zero_vec_def)
    27.8 -lemma vec_1[simp]: "vec 1 = 1" by (vector one_vec_def)
    27.9 +lemma vec_0[simp]: "vec 0 = 0" by vector
   27.10 +lemma vec_1[simp]: "vec 1 = 1" by vector
   27.11  
   27.12  lemma vec_inj[simp]: "vec x = vec y \<longleftrightarrow> x = y" by vector
   27.13  
   27.14  lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
   27.15  
   27.16 -lemma vec_add: "vec(x + y) = vec x + vec y"  by (vector vec_def)
   27.17 -lemma vec_sub: "vec(x - y) = vec x - vec y" by (vector vec_def)
   27.18 -lemma vec_cmul: "vec(c * x) = c *s vec x " by (vector vec_def)
   27.19 -lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def)
   27.20 +lemma vec_add: "vec(x + y) = vec x + vec y"  by vector
   27.21 +lemma vec_sub: "vec(x - y) = vec x - vec y" by vector
   27.22 +lemma vec_cmul: "vec(c * x) = c *s vec x " by vector
   27.23 +lemma vec_neg: "vec(- x) = - vec x " by vector
   27.24  
   27.25  lemma vec_setsum:
   27.26    assumes "finite S"
   27.27 @@ -164,7 +164,7 @@
   27.28  text{* Obvious "component-pushing". *}
   27.29  
   27.30  lemma vec_component [simp]: "vec x $ i = x"
   27.31 -  by (vector vec_def)
   27.32 +  by vector
   27.33  
   27.34  lemma vector_mult_component [simp]: "(x * y)$i = x$i * y$i"
   27.35    by vector
   27.36 @@ -330,7 +330,7 @@
   27.37    assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"
   27.38    shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) *  e"
   27.39    using setsum_norm_allsubsets_bound[OF assms]
   27.40 -  by (simp add: DIM_cart Basis_real_def)
   27.41 +  by simp
   27.42  
   27.43  subsection {* Matrix operations *}
   27.44  
    28.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Aug 10 14:31:06 2014 +0200
    28.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Aug 10 14:34:43 2014 +0200
    28.3 @@ -1502,7 +1502,7 @@
    28.4        by (intro convex_linear_vimage convex_translation convex_convex_hull,
    28.5          simp add: linear_iff)
    28.6      also have "?S = {y. (x, y) \<in> convex hull (s \<times> t)}"
    28.7 -      by (auto simp add: uminus_add_conv_diff image_def Bex_def)
    28.8 +      by (auto simp add: image_def Bex_def)
    28.9      finally show "convex {y. (x, y) \<in> convex hull (s \<times> t)}" .
   28.10    next
   28.11      show "convex {x. \<forall>y\<in>convex hull t. (x, y) \<in> convex hull (s \<times> t)}"
   28.12 @@ -1512,7 +1512,7 @@
   28.13        by (intro convex_linear_vimage convex_translation convex_convex_hull,
   28.14          simp add: linear_iff)
   28.15        also have "?S = {x. (x, y) \<in> convex hull (s \<times> t)}"
   28.16 -        by (auto simp add: uminus_add_conv_diff image_def Bex_def)
   28.17 +        by (auto simp add: image_def Bex_def)
   28.18        finally show "convex {x. (x, y) \<in> convex hull (s \<times> t)}" .
   28.19      qed
   28.20    qed
   28.21 @@ -5504,12 +5504,12 @@
   28.22      using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` s",
   28.23        OF convex_affinity compact_affinity]
   28.24      using assms(1,2)
   28.25 -    by (auto simp add: uminus_add_conv_diff scaleR_right_diff_distrib)
   28.26 +    by (auto simp add: scaleR_right_diff_distrib)
   28.27    then show ?thesis
   28.28      apply (rule_tac homeomorphic_trans[OF _ homeomorphic_balls(2)[of 1 _ ?n]])
   28.29      apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" s "?d *\<^sub>R -a"]])
   28.30      using `d>0` `e>0`
   28.31 -    apply (auto simp add: uminus_add_conv_diff scaleR_right_diff_distrib)
   28.32 +    apply (auto simp add: scaleR_right_diff_distrib)
   28.33      done
   28.34  qed
   28.35  
   28.36 @@ -5808,7 +5808,7 @@
   28.37    apply (rule_tac f="\<lambda>x. a + x" in arg_cong)
   28.38    apply (rule setsum.cong [OF refl])
   28.39    apply clarsimp
   28.40 -  apply (fast intro: set_plus_intro)
   28.41 +  apply fast
   28.42    done
   28.43  
   28.44  lemma box_eq_set_setsum_Basis:
   28.45 @@ -5895,7 +5895,7 @@
   28.46      apply (rule image_eqI[where x="{i. i\<in>Basis \<and> x\<bullet>i = 1}"])
   28.47      using as
   28.48      apply (subst euclidean_eq_iff)
   28.49 -    apply (auto simp: inner_setsum_left_Basis)
   28.50 +    apply auto
   28.51      done
   28.52  qed auto
   28.53  
   28.54 @@ -6430,7 +6430,7 @@
   28.55          apply (subst (asm) euclidean_eq_iff)
   28.56          using i
   28.57          apply (erule_tac x=i in ballE)
   28.58 -        apply (auto simp add:field_simps inner_simps)
   28.59 +        apply (auto simp add: field_simps inner_simps)
   28.60          done
   28.61        finally show "x \<bullet> i =
   28.62          ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) \<bullet> i"
   28.63 @@ -8138,8 +8138,7 @@
   28.64      and "convex S"
   28.65      and "rel_open S"
   28.66    shows "convex (f ` S) \<and> rel_open (f ` S)"
   28.67 -  by (metis assms convex_linear_image rel_interior_convex_linear_image
   28.68 -    linear_conv_bounded_linear rel_open_def)
   28.69 +  by (metis assms convex_linear_image rel_interior_convex_linear_image rel_open_def)
   28.70  
   28.71  lemma convex_rel_open_linear_preimage:
   28.72    fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
    29.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Aug 10 14:31:06 2014 +0200
    29.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Aug 10 14:34:43 2014 +0200
    29.3 @@ -69,7 +69,7 @@
    29.4  lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
    29.5      bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x within s)"
    29.6    unfolding has_derivative_def Lim
    29.7 -  by (auto simp add: netlimit_within inverse_eq_divide field_simps)
    29.8 +  by (auto simp add: netlimit_within field_simps)
    29.9  
   29.10  lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
   29.11      bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x)"
   29.12 @@ -1773,9 +1773,9 @@
   29.13          apply (rule lem3[rule_format])+
   29.14          done
   29.15        obtain N where N: "\<forall>h. norm (f' N x h - g' x h) \<le> 1 * norm h"
   29.16 -        using assms(3) `x \<in> s` by (fast intro: zero_less_one order_refl)
   29.17 +        using assms(3) `x \<in> s` by (fast intro: zero_less_one)
   29.18        have "bounded_linear (f' N x)"
   29.19 -        using assms(2) `x \<in> s` by (fast dest: has_derivative_bounded_linear)
   29.20 +        using assms(2) `x \<in> s` by fast
   29.21        from bounded_linear.bounded [OF this]
   29.22        obtain K where K: "\<forall>h. norm (f' N x h) \<le> norm h * K" ..
   29.23        {
    30.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Aug 10 14:31:06 2014 +0200
    30.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Aug 10 14:34:43 2014 +0200
    30.3 @@ -1125,7 +1125,7 @@
    30.4    note fin = this
    30.5    have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
    30.6      using f
    30.7 -    by (auto intro!: summable_ereal_pos summable_sums simp: ereal_le_real_iff zero_ereal_def)
    30.8 +    by (auto intro!: summable_ereal_pos simp: ereal_le_real_iff zero_ereal_def)
    30.9    also have "\<dots> = ereal r"
   30.10      using fin r by (auto simp: ereal_real)
   30.11    finally show "\<exists>r. (\<lambda>i. real (f i)) sums r"
   30.12 @@ -1252,7 +1252,8 @@
   30.13    apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union)
   30.14    apply (drule sym)
   30.15    apply auto
   30.16 -  by (metis INF_absorb centre_in_ball)
   30.17 +  apply (metis INF_absorb centre_in_ball)
   30.18 +  done
   30.19  
   30.20  
   30.21  lemma suminf_ereal_offset_le:
    31.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Aug 10 14:31:06 2014 +0200
    31.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sun Aug 10 14:34:43 2014 +0200
    31.3 @@ -343,7 +343,7 @@
    31.4                  using Basis_le_norm[OF k, of "?z - y"] unfolding dist_norm by auto
    31.5                then have "y\<bullet>k < a\<bullet>k"
    31.6                  using e[THEN conjunct1] k
    31.7 -                by (auto simp add: field_simps abs_less_iff as inner_Basis inner_simps)
    31.8 +                by (auto simp add: field_simps abs_less_iff as inner_simps)
    31.9                then have "y \<notin> i"
   31.10                  unfolding ab mem_box by (auto intro!: bexI[OF _ k])
   31.11                then show False using yi by auto
   31.12 @@ -12092,7 +12092,7 @@
   31.13      by (induct I) (auto intro!: bounded_linear_add bounded_linear_zero)
   31.14  next
   31.15    case False
   31.16 -  then show ?thesis by (simp add: bounded_linear_zero)
   31.17 +  then show ?thesis by simp
   31.18  qed
   31.19  
   31.20  lemma absolutely_integrable_vector_abs:
    32.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Aug 10 14:31:06 2014 +0200
    32.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Aug 10 14:34:43 2014 +0200
    32.3 @@ -7307,27 +7307,27 @@
    32.4  
    32.5  lemma real_affinity_le:
    32.6   "0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c \<le> y \<longleftrightarrow> x \<le> inverse(m) * y + -(c / m))"
    32.7 -  by (simp add: field_simps inverse_eq_divide)
    32.8 +  by (simp add: field_simps)
    32.9  
   32.10  lemma real_le_affinity:
   32.11   "0 < (m::'a::linordered_field) \<Longrightarrow> (y \<le> m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) \<le> x)"
   32.12 -  by (simp add: field_simps inverse_eq_divide)
   32.13 +  by (simp add: field_simps)
   32.14  
   32.15  lemma real_affinity_lt:
   32.16   "0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c < y \<longleftrightarrow> x < inverse(m) * y + -(c / m))"
   32.17 -  by (simp add: field_simps inverse_eq_divide)
   32.18 +  by (simp add: field_simps)
   32.19  
   32.20  lemma real_lt_affinity:
   32.21   "0 < (m::'a::linordered_field) \<Longrightarrow> (y < m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) < x)"
   32.22 -  by (simp add: field_simps inverse_eq_divide)
   32.23 +  by (simp add: field_simps)
   32.24  
   32.25  lemma real_affinity_eq:
   32.26   "(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (m * x + c = y \<longleftrightarrow> x = inverse(m) * y + -(c / m))"
   32.27 -  by (simp add: field_simps inverse_eq_divide)
   32.28 +  by (simp add: field_simps)
   32.29  
   32.30  lemma real_eq_affinity:
   32.31   "(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (y = m * x + c  \<longleftrightarrow> inverse(m) * y + -(c / m) = x)"
   32.32 -  by (simp add: field_simps inverse_eq_divide)
   32.33 +  by (simp add: field_simps)
   32.34  
   32.35  
   32.36  subsection {* Banach fixed point theorem (not really topological...) *}
    33.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Aug 10 14:31:06 2014 +0200
    33.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Aug 10 14:34:43 2014 +0200
    33.3 @@ -1336,7 +1336,14 @@
    33.4  
    33.5              val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss;
    33.6  
    33.7 -            val sel_default_eqs = map (prepare_term lthy) raw_sel_default_eqs;
    33.8 +            val sel_Tss = map (map (curry (op -->) fpT)) ctr_Tss;
    33.9 +            val sel_bTs =
   33.10 +              flat sel_bindingss ~~ flat sel_Tss
   33.11 +              |> filter_out (Binding.is_empty o fst)
   33.12 +              |> distinct (Binding.eq_name o pairself fst);
   33.13 +            val sel_default_lthy = fake_local_theory_for_sel_defaults sel_bTs lthy;
   33.14 +
   33.15 +            val sel_default_eqs = map (prepare_term sel_default_lthy) raw_sel_default_eqs;
   33.16  
   33.17              fun ctr_spec_of disc_b ctr0 sel_bs = ((disc_b, ctr0), sel_bs);
   33.18              val ctr_specs = map3 ctr_spec_of disc_bindings ctrs0 sel_bindingss;
   33.19 @@ -1570,7 +1577,8 @@
   33.20                        val thm = Goal.prove_sorry lthy [] [] goal
   33.21                            (fn {context = ctxt, prems = _} =>
   33.22                              mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
   33.23 -                              injects rel_inject_thms distincts rel_distinct_thms)
   33.24 +                              injects rel_inject_thms distincts rel_distinct_thms
   33.25 +                              (map rel_eq_of_bnf live_nesting_bnfs))
   33.26                          |> singleton (Proof_Context.export names_lthy lthy)
   33.27                          |> Thm.close_derivation;
   33.28  
    34.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sun Aug 10 14:31:06 2014 +0200
    34.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sun Aug 10 14:34:43 2014 +0200
    34.3 @@ -28,7 +28,7 @@
    34.4    val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
    34.5      tactic
    34.6    val mk_rel_cases_tac:  Proof.context -> cterm -> cterm -> thm -> thm list -> thm list ->
    34.7 -    thm list -> thm list -> tactic
    34.8 +    thm list -> thm list -> thm list -> tactic
    34.9    val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
   34.10      thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
   34.11      thm list -> thm list -> thm list -> tactic
   34.12 @@ -217,11 +217,11 @@
   34.13        (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
   34.14        selsss));
   34.15  
   34.16 -fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts =
   34.17 +fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs=
   34.18    HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
   34.19      rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
   34.20        hyp_subst_tac ctxt) THEN
   34.21 -  unfold_thms_tac ctxt (injects @ rel_injects @ @{thms conj_imp_eq_imp_imp simp_thms(6)
   34.22 +  unfold_thms_tac ctxt (rel_eqs @ injects @ rel_injects @ @{thms conj_imp_eq_imp_imp simp_thms(6)
   34.23      True_implies_equals conj_imp_eq_imp_imp} @
   34.24      map (fn thm => thm RS eqFalseI) (distincts @ rel_distincts) @
   34.25      map (fn thm => thm RS eqTrueI) rel_injects) THEN
   34.26 @@ -261,7 +261,7 @@
   34.27          unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
   34.28            @{thms BNF_Comp.id_bnf_comp_def vimage2p_def}) THEN
   34.29          TRYALL (hyp_subst_tac ctxt) THEN
   34.30 -        unfold_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
   34.31 +        unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
   34.32            Inr_Inl_False  sum.inject prod.inject}) THEN
   34.33          TRYALL (etac FalseE ORELSE' (REPEAT_DETERM o etac conjE) THEN' atac))
   34.34      cterms exhausts ctor_defss ctor_injects rel_pre_list_defs Abs_inverses);
   34.35 @@ -270,7 +270,7 @@
   34.36    HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
   34.37      rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
   34.38        hyp_subst_tac ctxt) THEN
   34.39 -  Local_Defs.unfold_tac ctxt (sels @ rel_injects @ @{thms simp_thms(6,7,8,11,12,15,16,21,22,24)} @
   34.40 +  unfold_thms_tac ctxt (sels @ rel_injects @ @{thms simp_thms(6,7,8,11,12,15,16,21,22,24)} @
   34.41      ((discs @ distincts) RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @
   34.42      (rel_injects RL @{thms iffD2[OF eq_True]}) @
   34.43      (rel_distincts RL @{thms iffD2[OF eq_False]})) THEN
    35.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun Aug 10 14:31:06 2014 +0200
    35.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun Aug 10 14:34:43 2014 +0200
    35.3 @@ -62,6 +62,7 @@
    35.4    val ctr_of_ctr_spec: ('c, 'a) ctr_spec -> 'c
    35.5    val args_of_ctr_spec: ('c, 'a) ctr_spec -> 'a list
    35.6  
    35.7 +  val fake_local_theory_for_sel_defaults: (binding * typ) list -> Proof.context -> Proof.context
    35.8    val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
    35.9      (((bool * bool) * binding) * (term, binding) ctr_spec list) * term list -> local_theory ->
   35.10      ctr_sugar * local_theory
   35.11 @@ -328,6 +329,12 @@
   35.12        malformed ()
   35.13    end;
   35.14  
   35.15 +(* Ideally, we would enrich the context with constants rather than free variables. *)
   35.16 +fun fake_local_theory_for_sel_defaults sel_bTs =
   35.17 +  Proof_Context.allow_dummies
   35.18 +  #> Proof_Context.add_fixes (map (fn (b, T) => (b, SOME T, NoSyn)) sel_bTs)
   35.19 +  #> snd;
   35.20 +
   35.21  type ('c, 'a) ctr_spec = (binding * 'c) * 'a list;
   35.22  
   35.23  fun disc_of_ctr_spec ((disc, _), _) = disc;
   35.24 @@ -501,30 +508,35 @@
   35.25          (true, [], [], [], [], [], lthy')
   35.26        else
   35.27          let
   35.28 -          val sel_bindings = flat sel_bindingss;
   35.29 -          val uniq_sel_bindings = distinct Binding.eq_name sel_bindings;
   35.30 -          val all_sels_distinct = (length uniq_sel_bindings = length sel_bindings);
   35.31 +          val all_sel_bindings = flat sel_bindingss;
   35.32 +          val num_all_sel_bindings = length all_sel_bindings;
   35.33 +          val uniq_sel_bindings = distinct Binding.eq_name all_sel_bindings;
   35.34 +          val all_sels_distinct = (length uniq_sel_bindings = num_all_sel_bindings);
   35.35  
   35.36            val sel_binding_index =
   35.37 -            if all_sels_distinct then 1 upto length sel_bindings
   35.38 -            else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) sel_bindings;
   35.39 +            if all_sels_distinct then
   35.40 +              1 upto num_all_sel_bindings
   35.41 +            else
   35.42 +              map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) all_sel_bindings;
   35.43  
   35.44 -          val all_proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss);
   35.45 +          val all_proto_sels = flat (map3 (fn k => fn xs => map (pair k o pair xs)) ks xss xss);
   35.46            val sel_infos =
   35.47              AList.group (op =) (sel_binding_index ~~ all_proto_sels)
   35.48              |> sort (int_ord o pairself fst)
   35.49              |> map snd |> curry (op ~~) uniq_sel_bindings;
   35.50            val sel_bindings = map fst sel_infos;
   35.51 -          val sel_Ts = map (curry (op -->) fcT o fastype_of o snd o snd o hd o snd) sel_infos;
   35.52 -
   35.53 -          val sel_default_lthy = no_defs_lthy
   35.54 -            |> Proof_Context.allow_dummies
   35.55 -            |> Proof_Context.add_fixes
   35.56 -              (map2 (fn b => fn T => (b, SOME T, NoSyn)) sel_bindings sel_Ts)
   35.57 -            |> snd;
   35.58  
   35.59            val sel_defaults =
   35.60 -            map (extract_sel_default sel_default_lthy o prep_term sel_default_lthy) sel_default_eqs;
   35.61 +            if null sel_default_eqs then
   35.62 +              []
   35.63 +            else
   35.64 +              let
   35.65 +                val sel_Ts = map (curry (op -->) fcT o fastype_of o snd o snd o hd o snd) sel_infos;
   35.66 +                val fake_lthy =
   35.67 +                  fake_local_theory_for_sel_defaults (sel_bindings ~~ sel_Ts) no_defs_lthy;
   35.68 +              in
   35.69 +                map (extract_sel_default fake_lthy o prep_term fake_lthy) sel_default_eqs
   35.70 +              end;
   35.71  
   35.72            fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT);
   35.73  
    36.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sun Aug 10 14:31:06 2014 +0200
    36.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sun Aug 10 14:34:43 2014 +0200
    36.3 @@ -119,11 +119,13 @@
    36.4    end
    36.5  
    36.6  fun thms_in_proof max_thms name_tabs th =
    36.7 -  let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in
    36.8 -    SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names
    36.9 -      (Proofterm.strip_thm (Thm.proof_body_of th)))
   36.10 -    handle TOO_MANY () => NONE
   36.11 -  end
   36.12 +  (case try Thm.proof_body_of th of
   36.13 +    NONE => NONE
   36.14 +  | SOME body =>
   36.15 +    let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in
   36.16 +      SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names (Proofterm.strip_thm body))
   36.17 +      handle TOO_MANY () => NONE
   36.18 +    end)
   36.19  
   36.20  fun thms_of_name ctxt name =
   36.21    let
    37.1 --- a/src/HOL/Tools/inductive_set.ML	Sun Aug 10 14:31:06 2014 +0200
    37.2 +++ b/src/HOL/Tools/inductive_set.ML	Sun Aug 10 14:34:43 2014 +0200
    37.3 @@ -275,7 +275,9 @@
    37.4                     Sign.typ_instance thy (U, T'))
    37.5                       (Symtab.lookup_list set_arities s')
    37.6                   then
    37.7 -                   (warning ("Ignoring conversion rule for operator " ^ s'); tab)
    37.8 +                   (if Context_Position.is_really_visible ctxt then
    37.9 +                     warning ("Ignoring conversion rule for operator " ^ s')
   37.10 +                    else (); tab)
   37.11                   else
   37.12                     {to_set_simps = thm :: to_set_simps,
   37.13                      to_pred_simps =
   37.14 @@ -289,8 +291,14 @@
   37.15         | _ => raise Malformed "equation between predicates expected")
   37.16    | _ => raise Malformed "equation expected")
   37.17    handle Malformed msg =>
   37.18 -    (warning ("Ignoring malformed set / predicate conversion rule: " ^ msg ^
   37.19 -      "\n" ^ Display.string_of_thm (Context.proof_of context) thm); tab);
   37.20 +    let
   37.21 +      val ctxt = Context.proof_of context
   37.22 +      val _ =
   37.23 +        if Context_Position.is_really_visible ctxt then
   37.24 +          warning ("Ignoring malformed set / predicate conversion rule: " ^ msg ^
   37.25 +            "\n" ^ Display.string_of_thm ctxt thm)
   37.26 +        else ();
   37.27 +    in tab end;
   37.28  
   37.29  val pred_set_conv_att = Thm.declaration_attribute
   37.30    (fn thm => fn ctxt => Data.map (add ctxt thm) ctxt);
    38.1 --- a/src/Provers/classical.ML	Sun Aug 10 14:31:06 2014 +0200
    38.2 +++ b/src/Provers/classical.ML	Sun Aug 10 14:34:43 2014 +0200
    38.3 @@ -309,7 +309,7 @@
    38.4    else Tactic.make_elim th;
    38.5  
    38.6  fun warn_thm (SOME (Context.Proof ctxt)) msg th =
    38.7 -      if Context_Position.is_visible ctxt
    38.8 +      if Context_Position.is_really_visible ctxt
    38.9        then warning (msg ^ Display.string_of_thm ctxt th) else ()
   38.10    | warn_thm _ _ _ = ();
   38.11  
    39.1 --- a/src/Pure/GUI/gui.scala	Sun Aug 10 14:31:06 2014 +0200
    39.2 +++ b/src/Pure/GUI/gui.scala	Sun Aug 10 14:34:43 2014 +0200
    39.3 @@ -12,7 +12,7 @@
    39.4  import java.awt.{Image, Component, Container, Toolkit, Window, Font, KeyboardFocusManager}
    39.5  import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
    39.6  import java.awt.geom.AffineTransform
    39.7 -import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow,
    39.8 +import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JDialog,
    39.9    JButton, JTextField}
   39.10  
   39.11  import scala.collection.convert.WrapAsJava
   39.12 @@ -208,8 +208,9 @@
   39.13  
   39.14    def layered_pane(component: Component): Option[JLayeredPane] =
   39.15      parent_window(component) match {
   39.16 -      case Some(window: JWindow) => Some(window.getLayeredPane)
   39.17 -      case Some(frame: JFrame) => Some(frame.getLayeredPane)
   39.18 +      case Some(w: JWindow) => Some(w.getLayeredPane)
   39.19 +      case Some(w: JFrame) => Some(w.getLayeredPane)
   39.20 +      case Some(w: JDialog) => Some(w.getLayeredPane)
   39.21        case _ => None
   39.22      }
   39.23  
    40.1 --- a/src/Pure/General/exn.scala	Sun Aug 10 14:31:06 2014 +0200
    40.2 +++ b/src/Pure/General/exn.scala	Sun Aug 10 14:34:43 2014 +0200
    40.3 @@ -82,7 +82,7 @@
    40.4      }
    40.5      else if (exn.getClass == runtime_exception) {
    40.6        val msg = exn.getMessage
    40.7 -      Some(if (msg == null) "Error" else msg)
    40.8 +      Some(if (msg == null || msg == "") "Error" else msg)
    40.9      }
   40.10      else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
   40.11      else None
    41.1 --- a/src/Pure/General/symbol.scala	Sun Aug 10 14:31:06 2014 +0200
    41.2 +++ b/src/Pure/General/symbol.scala	Sun Aug 10 14:34:43 2014 +0200
    41.3 @@ -203,6 +203,8 @@
    41.4          case _ => false
    41.5        }
    41.6  
    41.7 +    override def toString: String = "Text_Chunk" + range.toString
    41.8 +
    41.9      def decode(symbol_offset: Offset): Text.Offset = index.decode(symbol_offset)
   41.10      def decode(symbol_range: Range): Text.Range = index.decode(symbol_range)
   41.11      def incorporate(symbol_range: Range): Option[Text.Range] =
    42.1 --- a/src/Pure/Isar/attrib.ML	Sun Aug 10 14:31:06 2014 +0200
    42.2 +++ b/src/Pure/Isar/attrib.ML	Sun Aug 10 14:34:43 2014 +0200
    42.3 @@ -292,7 +292,7 @@
    42.4  in
    42.5  
    42.6  fun partial_evaluation ctxt facts =
    42.7 -  (facts, Context.Proof ctxt) |->
    42.8 +  (facts, Context.Proof (Context_Position.not_really ctxt)) |->
    42.9      fold_map (fn ((b, more_atts), fact) => fn context =>
   42.10        let
   42.11          val (fact', (decls, context')) =
    43.1 --- a/src/Pure/Isar/element.ML	Sun Aug 10 14:31:06 2014 +0200
    43.2 +++ b/src/Pure/Isar/element.ML	Sun Aug 10 14:34:43 2014 +0200
    43.3 @@ -51,6 +51,7 @@
    43.4    val satisfy_morphism: witness list -> morphism
    43.5    val eq_morphism: theory -> thm list -> morphism option
    43.6    val init: context_i -> Context.generic -> Context.generic
    43.7 +  val init': context_i -> Context.generic -> Context.generic
    43.8    val activate_i: context_i -> Proof.context -> context_i * Proof.context
    43.9    val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
   43.10  end;
   43.11 @@ -473,18 +474,16 @@
   43.12  
   43.13  (* init *)
   43.14  
   43.15 -local
   43.16 -
   43.17 -fun init0 (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
   43.18 -  | init0 (Constrains _) = I
   43.19 -  | init0 (Assumes asms) = Context.map_proof (fn ctxt =>
   43.20 +fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
   43.21 +  | init (Constrains _) = I
   43.22 +  | init (Assumes asms) = Context.map_proof (fn ctxt =>
   43.23        let
   43.24          val asms' = Attrib.map_specs (map (Attrib.attribute ctxt)) asms;
   43.25          val (_, ctxt') = ctxt
   43.26            |> fold Variable.auto_fixes (maps (map #1 o #2) asms')
   43.27            |> Proof_Context.add_assms_i Assumption.assume_export asms';
   43.28        in ctxt' end)
   43.29 -  | init0 (Defines defs) = Context.map_proof (fn ctxt =>
   43.30 +  | init (Defines defs) = Context.map_proof (fn ctxt =>
   43.31        let
   43.32          val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
   43.33          val asms = defs' |> map (fn (b, (t, ps)) =>
   43.34 @@ -494,17 +493,15 @@
   43.35            |> fold Variable.auto_fixes (map #1 asms)
   43.36            |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
   43.37        in ctxt' end)
   43.38 -  | init0 (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
   43.39 +  | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
   43.40  
   43.41 -in
   43.42 -
   43.43 -fun init elem context =
   43.44 +fun init' elem context =
   43.45    context
   43.46 -  |> Context.mapping I Thm.unchecked_hyps
   43.47 -  |> init0 elem
   43.48 -  |> Context.mapping I (fn ctxt => Thm.restore_hyps (Context.proof_of context) ctxt);
   43.49 -
   43.50 -end;
   43.51 +  |> Context.mapping I (Thm.unchecked_hyps #> Context_Position.not_really)
   43.52 +  |> init elem
   43.53 +  |> Context.mapping I (fn ctxt =>
   43.54 +      let val ctxt0 = Context.proof_of context
   43.55 +      in ctxt |> Context_Position.restore_visible ctxt0 |> Thm.restore_hyps ctxt0 end);
   43.56  
   43.57  
   43.58  (* activate *)
    44.1 --- a/src/Pure/Isar/expression.ML	Sun Aug 10 14:31:06 2014 +0200
    44.2 +++ b/src/Pure/Isar/expression.ML	Sun Aug 10 14:34:43 2014 +0200
    44.3 @@ -865,8 +865,8 @@
    44.4  
    44.5  (* generic interpretation machinery *)
    44.6  
    44.7 -fun meta_rewrite eqns ctxt =
    44.8 -  (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
    44.9 +fun meta_rewrite ctxt eqns =
   44.10 +  map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns);
   44.11  
   44.12  fun note_eqns_register note activate deps witss eqns attrss export export' ctxt =
   44.13    let
   44.14 @@ -874,7 +874,7 @@
   44.15        (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
   44.16      val (eqns', ctxt') = ctxt
   44.17        |> note Thm.lemmaK facts
   44.18 -      |-> meta_rewrite;
   44.19 +      |> (fn (eqns, ctxt') => (meta_rewrite ctxt' eqns, ctxt'));
   44.20      val dep_morphs =
   44.21        map2 (fn (dep, morph) => fn wits =>
   44.22            (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)))
    45.1 --- a/src/Pure/Isar/keyword.scala	Sun Aug 10 14:31:06 2014 +0200
    45.2 +++ b/src/Pure/Isar/keyword.scala	Sun Aug 10 14:34:43 2014 +0200
    45.3 @@ -44,21 +44,31 @@
    45.4  
    45.5    /* categories */
    45.6  
    45.7 -  val minor = Set(MINOR)
    45.8 +  val diag = Set(DIAG)
    45.9    val control = Set(CONTROL)
   45.10 -  val diag = Set(DIAG)
   45.11 +
   45.12 +  val heading = Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
   45.13 +    PRF_HEADING2, PRF_HEADING3, PRF_HEADING4)
   45.14 +
   45.15    val theory =
   45.16      Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
   45.17 -      THY_DECL, THY_GOAL)
   45.18 -  val theory1 = Set(THY_BEGIN, THY_END)
   45.19 -  val theory2 = Set(THY_DECL, THY_GOAL)
   45.20 +      THY_LOAD, THY_DECL, THY_GOAL)
   45.21 +
   45.22 +  val theory_body =
   45.23 +    Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, THY_LOAD, THY_DECL, THY_GOAL)
   45.24 +
   45.25    val proof =
   45.26      Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4,
   45.27 -      PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL,
   45.28 -      PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
   45.29 -  val proof1 =
   45.30 -    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
   45.31 -      PRF_CHAIN, PRF_DECL)
   45.32 -  val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
   45.33 +      PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL,
   45.34 +      PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
   45.35 +
   45.36 +  val proof_body =
   45.37 +    Set(DIAG, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN,
   45.38 +      PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
   45.39 +
   45.40 +  val theory_goal = Set(THY_GOAL)
   45.41 +  val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
   45.42 +  val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
   45.43 +  val qed_global = Set(QED_GLOBAL)
   45.44  }
   45.45  
    46.1 --- a/src/Pure/Isar/locale.ML	Sun Aug 10 14:31:06 2014 +0200
    46.2 +++ b/src/Pure/Isar/locale.ML	Sun Aug 10 14:34:43 2014 +0200
    46.3 @@ -448,7 +448,7 @@
    46.4    let
    46.5      val thy = Context.theory_of context;
    46.6      val activate =
    46.7 -      activate_notes Element.init
    46.8 +      activate_notes Element.init'
    46.9          (Morphism.transfer_morphism o Context.theory_of) context export;
   46.10    in
   46.11      roundup thy activate (the_default Morphism.identity export) dep (Idents.get context, context)
   46.12 @@ -460,7 +460,7 @@
   46.13      val context = Context.Proof (Proof_Context.init_global thy);
   46.14      val marked = Idents.get context;
   46.15      val (marked', context') = (empty_idents, context)
   46.16 -      |> activate_all name thy Element.init (Morphism.transfer_morphism o Context.theory_of);
   46.17 +      |> activate_all name thy Element.init' (Morphism.transfer_morphism o Context.theory_of);
   46.18    in
   46.19      context'
   46.20      |> Idents.put (merge_idents (marked, marked'))
    47.1 --- a/src/Pure/Isar/method.ML	Sun Aug 10 14:31:06 2014 +0200
    47.2 +++ b/src/Pure/Isar/method.ML	Sun Aug 10 14:34:43 2014 +0200
    47.3 @@ -347,10 +347,11 @@
    47.4    let val table = get_methods ctxt
    47.5    in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
    47.6  
    47.7 -fun method_closure ctxt src0 =
    47.8 +fun method_closure ctxt0 src0 =
    47.9    let
   47.10 -    val (src1, meth) = check_src ctxt src0;
   47.11 +    val (src1, meth) = check_src ctxt0 src0;
   47.12      val src2 = Args.init_assignable src1;
   47.13 +    val ctxt = Context_Position.not_really ctxt0;
   47.14      val _ = Seq.pull (apply (method ctxt src2) ctxt [] (Goal.protect 0 Drule.dummy_thm));
   47.15    in Args.closure src2 end;
   47.16  
    48.1 --- a/src/Pure/Isar/runtime.ML	Sun Aug 10 14:31:06 2014 +0200
    48.2 +++ b/src/Pure/Isar/runtime.ML	Sun Aug 10 14:34:43 2014 +0200
    48.3 @@ -99,6 +99,7 @@
    48.4                TERMINATE => "Exit"
    48.5              | TimeLimit.TimeOut => "Timeout"
    48.6              | TOPLEVEL_ERROR => "Error"
    48.7 +            | ERROR "" => "Error"
    48.8              | ERROR msg => msg
    48.9              | Fail msg => raised exn "Fail" [msg]
   48.10              | THEORY (msg, thys) =>
    49.1 --- a/src/Pure/ML-Systems/polyml.ML	Sun Aug 10 14:31:06 2014 +0200
    49.2 +++ b/src/Pure/ML-Systems/polyml.ML	Sun Aug 10 14:34:43 2014 +0200
    49.3 @@ -174,5 +174,5 @@
    49.4      ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
    49.5  
    49.6  val ml_make_string =
    49.7 -  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Options.get_print_depth ())))))";
    49.8 +  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, Isabelle.ML_print_depth ())))))";
    49.9  
    50.1 --- a/src/Pure/ML/ml_antiquotation.ML	Sun Aug 10 14:31:06 2014 +0200
    50.2 +++ b/src/Pure/ML/ml_antiquotation.ML	Sun Aug 10 14:34:43 2014 +0200
    50.3 @@ -19,7 +19,7 @@
    50.4  
    50.5  (* unique names *)
    50.6  
    50.7 -val init_context = ML_Syntax.reserved |> Name.declare "ML_context";
    50.8 +val init_context = ML_Syntax.reserved |> fold Name.declare ["ML_context", "ML_print_depth"];
    50.9  
   50.10  structure Names = Proof_Data
   50.11  (
    51.1 --- a/src/Pure/ML/ml_context.ML	Sun Aug 10 14:31:06 2014 +0200
    51.2 +++ b/src/Pure/ML/ml_context.ML	Sun Aug 10 14:34:43 2014 +0200
    51.3 @@ -93,7 +93,10 @@
    51.4    ML_Lex.tokenize
    51.5      ("structure Isabelle =\nstruct\n\
    51.6       \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
    51.7 -     " (ML_Context.the_local_context ());\n");
    51.8 +     " (ML_Context.the_local_context ());\n\
    51.9 +     \val ML_print_depth =\n\
   51.10 +     \  let val default = ML_Options.get_print_depth ()\n\
   51.11 +     \  in fn () => ML_Options.get_print_depth_default default end;\n");
   51.12  
   51.13  val end_env = ML_Lex.tokenize "end;";
   51.14  val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";
    52.1 --- a/src/Pure/ML/ml_options.ML	Sun Aug 10 14:31:06 2014 +0200
    52.2 +++ b/src/Pure/ML/ml_options.ML	Sun Aug 10 14:34:43 2014 +0200
    52.3 @@ -14,6 +14,7 @@
    52.4    val print_depth_raw: Config.raw
    52.5    val print_depth: int Config.T
    52.6    val get_print_depth: unit -> int
    52.7 +  val get_print_depth_default: int -> int
    52.8  end;
    52.9  
   52.10  structure ML_Options: ML_OPTIONS =
   52.11 @@ -47,4 +48,9 @@
   52.12      NONE => get_default_print_depth ()
   52.13    | SOME context => Config.get_generic context print_depth);
   52.14  
   52.15 +fun get_print_depth_default default =
   52.16 +  (case Context.thread_data () of
   52.17 +    NONE => default
   52.18 +  | SOME context => Config.get_generic context print_depth);
   52.19 +
   52.20  end;
    53.1 --- a/src/Pure/PIDE/command.ML	Sun Aug 10 14:31:06 2014 +0200
    53.2 +++ b/src/Pure/PIDE/command.ML	Sun Aug 10 14:34:43 2014 +0200
    53.3 @@ -204,7 +204,7 @@
    53.4    in
    53.5      (case res of
    53.6        NONE => st0
    53.7 -    | SOME st => (warning (Toplevel.type_error tr st0 ^ " -- resetting state"); st))
    53.8 +    | SOME st => (Output.error_message (Toplevel.type_error tr st0 ^ " -- using reset state"); st))
    53.9    end) ();
   53.10  
   53.11  fun run int tr st =
   53.12 @@ -382,7 +382,7 @@
   53.13    print_function "Execution.print"
   53.14      (fn {args, exec_id, ...} =>
   53.15        if null args then
   53.16 -        SOME {delay = NONE, pri = 1, persistent = false, strict = true,
   53.17 +        SOME {delay = NONE, pri = 1, persistent = false, strict = false,
   53.18            print_fn = fn _ => fn _ => Execution.fork_prints exec_id}
   53.19        else NONE);
   53.20  
    54.1 --- a/src/Pure/PIDE/command.scala	Sun Aug 10 14:31:06 2014 +0200
    54.2 +++ b/src/Pure/PIDE/command.scala	Sun Aug 10 14:34:43 2014 +0200
    54.3 @@ -356,14 +356,14 @@
    54.4  
    54.5    /* blobs */
    54.6  
    54.7 -  def blobs_changed(doc_blobs: Document.Blobs): Boolean =
    54.8 -    blobs.exists({ case Exn.Res((name, _)) => doc_blobs.changed(name) case _ => false })
    54.9 -
   54.10    def blobs_names: List[Document.Node.Name] =
   54.11      for (Exn.Res((name, _)) <- blobs) yield name
   54.12  
   54.13 -  def blobs_digests: List[SHA1.Digest] =
   54.14 -    for (Exn.Res((_, Some((digest, _)))) <- blobs) yield digest
   54.15 +  def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] =
   54.16 +    for (Exn.Res((name, Some((digest, _)))) <- blobs) yield (name, digest)
   54.17 +
   54.18 +  def blobs_changed(doc_blobs: Document.Blobs): Boolean =
   54.19 +    blobs.exists({ case Exn.Res((name, _)) => doc_blobs.changed(name) case _ => false })
   54.20  
   54.21  
   54.22    /* source chunks */
    55.1 --- a/src/Pure/PIDE/document.ML	Sun Aug 10 14:31:06 2014 +0200
    55.2 +++ b/src/Pure/PIDE/document.ML	Sun Aug 10 14:34:43 2014 +0200
    55.3 @@ -48,7 +48,7 @@
    55.4   {required: bool,  (*required node*)
    55.5    visible: Inttab.set,  (*visible commands*)
    55.6    visible_last: Document_ID.command option,  (*last visible command*)
    55.7 -  overlays: (string * string list) list Inttab.table};  (*command id -> print function with args*)
    55.8 +  overlays: (string * string list) list Inttab.table};  (*command id -> print functions with args*)
    55.9  
   55.10  structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord);
   55.11  
    56.1 --- a/src/Pure/PIDE/document.scala	Sun Aug 10 14:31:06 2014 +0200
    56.2 +++ b/src/Pure/PIDE/document.scala	Sun Aug 10 14:34:43 2014 +0200
    56.3 @@ -58,10 +58,6 @@
    56.4  
    56.5    final class Blobs private(blobs: Map[Node.Name, Blob])
    56.6    {
    56.7 -    private lazy val digests: Map[SHA1.Digest, Blob] =
    56.8 -      for ((_, blob) <- blobs) yield (blob.bytes.sha1_digest, blob)
    56.9 -
   56.10 -    def get(digest: SHA1.Digest): Option[Blob] = digests.get(digest)
   56.11      def get(name: Node.Name): Option[Blob] = blobs.get(name)
   56.12  
   56.13      def changed(name: Node.Name): Boolean =
   56.14 @@ -648,7 +644,7 @@
   56.15          (_, node) <- version.nodes.iterator
   56.16          command <- node.commands.iterator
   56.17        } {
   56.18 -        for (digest <- command.blobs_digests; if !blobs1.contains(digest))
   56.19 +        for ((_, digest) <- command.blobs_defined; if !blobs1.contains(digest))
   56.20            blobs1 += digest
   56.21  
   56.22          if (!commands1.isDefinedAt(command.id))
    57.1 --- a/src/Pure/PIDE/protocol.ML	Sun Aug 10 14:31:06 2014 +0200
    57.2 +++ b/src/Pure/PIDE/protocol.ML	Sun Aug 10 14:34:43 2014 +0200
    57.3 @@ -123,5 +123,9 @@
    57.4            | Exn.Exn exn => (Runtime.exn_error_message exn; false));
    57.5      in Output.protocol_message (Markup.use_theories_result id ok) [] end);
    57.6  
    57.7 +val _ =
    57.8 +  Isabelle_Process.protocol_command "ML_System.share_common_data"
    57.9 +    (fn [] => ML_System.share_common_data ());
   57.10 +
   57.11  end;
   57.12  
    58.1 --- a/src/Pure/PIDE/protocol.scala	Sun Aug 10 14:31:06 2014 +0200
    58.2 +++ b/src/Pure/PIDE/protocol.scala	Sun Aug 10 14:34:43 2014 +0200
    58.3 @@ -145,8 +145,8 @@
    58.4        val status = Status.merge(states.iterator.map(_.protocol_status))
    58.5  
    58.6        if (status.is_running) running += 1
    58.7 +      else if (status.is_failed) failed += 1
    58.8        else if (status.is_warned) warned += 1
    58.9 -      else if (status.is_failed) failed += 1
   58.10        else if (status.is_finished) finished += 1
   58.11        else unprocessed += 1
   58.12      }
    59.1 --- a/src/Pure/PIDE/query_operation.ML	Sun Aug 10 14:31:06 2014 +0200
    59.2 +++ b/src/Pure/PIDE/query_operation.ML	Sun Aug 10 14:34:43 2014 +0200
    59.3 @@ -2,7 +2,7 @@
    59.4      Author:     Makarius
    59.5  
    59.6  One-shot query operations via asynchronous print functions and temporary
    59.7 -document overlay.
    59.8 +document overlays.
    59.9  *)
   59.10  
   59.11  signature QUERY_OPERATION =
    60.1 --- a/src/Pure/PIDE/session.scala	Sun Aug 10 14:31:06 2014 +0200
    60.2 +++ b/src/Pure/PIDE/session.scala	Sun Aug 10 14:34:43 2014 +0200
    60.3 @@ -47,7 +47,6 @@
    60.4  
    60.5    sealed case class Change(
    60.6      previous: Document.Version,
    60.7 -    doc_blobs: Document.Blobs,
    60.8      syntax_changed: Boolean,
    60.9      deps_changed: Boolean,
   60.10      doc_edits: List[Document.Edit_Command],
   60.11 @@ -177,8 +176,7 @@
   60.12    /* tuning parameters */
   60.13  
   60.14    def output_delay: Time = Time.seconds(0.1)  // prover output (markup, common messages)
   60.15 -  def message_delay: Time = Time.seconds(0.1)  // prover input/output messages
   60.16 -  def prune_delay: Time = Time.seconds(60.0)  // prune history -- delete old versions
   60.17 +  def prune_delay: Time = Time.seconds(60.0)  // prune history (delete old versions)
   60.18    def prune_size: Int = 0  // size of retained history
   60.19    def syslog_limit: Int = 100
   60.20    def reparse_limit: Int = 0
   60.21 @@ -380,15 +378,15 @@
   60.22        def id_command(command: Command)
   60.23        {
   60.24          for {
   60.25 -          digest <- command.blobs_digests
   60.26 +          (name, digest) <- command.blobs_defined
   60.27            if !global_state.value.defined_blob(digest)
   60.28          } {
   60.29 -          change.doc_blobs.get(digest) match {
   60.30 +          change.version.nodes(name).get_blob match {
   60.31              case Some(blob) =>
   60.32                global_state.change(_.define_blob(digest))
   60.33                prover.get.define_blob(digest, blob.bytes)
   60.34              case None =>
   60.35 -              Output.error_message("Missing blob for SHA1 digest " + digest)
   60.36 +              Output.error_message("Missing blob " + quote(name.toString))
   60.37            }
   60.38          }
   60.39  
    61.1 --- a/src/Pure/Thy/thy_syntax.scala	Sun Aug 10 14:31:06 2014 +0200
    61.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sun Aug 10 14:34:43 2014 +0200
    61.3 @@ -490,6 +490,6 @@
    61.4          (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(Some(syntax), nodes))
    61.5        }
    61.6  
    61.7 -    Session.Change(previous, doc_blobs, syntax_changed, deps_changed, doc_edits, version)
    61.8 +    Session.Change(previous, syntax_changed, deps_changed, doc_edits, version)
    61.9    }
   61.10  }
    62.1 --- a/src/Pure/Tools/ml_statistics.scala	Sun Aug 10 14:31:06 2014 +0200
    62.2 +++ b/src/Pure/Tools/ml_statistics.scala	Sun Aug 10 14:34:43 2014 +0200
    62.3 @@ -33,6 +33,12 @@
    62.4  
    62.5    /* standard fields */
    62.6  
    62.7 +  val tasks_fields =
    62.8 +    ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
    62.9 +
   62.10 +  val workers_fields =
   62.11 +    ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
   62.12 +
   62.13    val GC_fields = ("GCs", List("partial_GCs", "full_GCs"))
   62.14  
   62.15    val heap_fields =
   62.16 @@ -47,15 +53,9 @@
   62.17  
   62.18    val speed_fields = ("Speed", List("speed_CPU", "speed_GC"))
   62.19  
   62.20 -  val tasks_fields =
   62.21 -    ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
   62.22 -
   62.23 -  val workers_fields =
   62.24 -    ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
   62.25 -
   62.26    val standard_fields =
   62.27 -    List(GC_fields, heap_fields, threads_fields, time_fields, speed_fields,
   62.28 -      tasks_fields, workers_fields)
   62.29 +    List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields,
   62.30 +      time_fields, speed_fields)
   62.31  }
   62.32  
   62.33  final class ML_Statistics private(val name: String, val stats: List[Properties.T])
    63.1 --- a/src/Pure/config.ML	Sun Aug 10 14:31:06 2014 +0200
    63.2 +++ b/src/Pure/config.ML	Sun Aug 10 14:34:43 2014 +0200
    63.3 @@ -130,13 +130,10 @@
    63.4      fun map_value f (context as Context.Proof ctxt) =
    63.5            let val context' = update_value f context in
    63.6              if global andalso
    63.7 -              Context_Position.is_visible ctxt andalso
    63.8 +              Context_Position.is_really_visible ctxt andalso
    63.9                print_value (get_value (Context.Theory (Context.theory_of context'))) <>
   63.10                  print_value (get_value context')
   63.11 -            then
   63.12 -             (if Context_Position.is_visible ctxt then
   63.13 -                warning ("Ignoring local change of global option " ^ quote name)
   63.14 -              else (); context)
   63.15 +            then (warning ("Ignoring local change of global option " ^ quote name); context)
   63.16              else context'
   63.17            end
   63.18        | map_value f context = update_value f context;
    64.1 --- a/src/Pure/context_position.ML	Sun Aug 10 14:31:06 2014 +0200
    64.2 +++ b/src/Pure/context_position.ML	Sun Aug 10 14:34:43 2014 +0200
    64.3 @@ -11,6 +11,8 @@
    64.4    val is_visible_global: theory -> bool
    64.5    val set_visible: bool -> Proof.context -> Proof.context
    64.6    val set_visible_global: bool -> theory -> theory
    64.7 +  val is_really_visible: Proof.context -> bool
    64.8 +  val not_really: Proof.context -> Proof.context
    64.9    val restore_visible: Proof.context -> Proof.context -> Proof.context
   64.10    val restore_visible_global: theory -> theory -> theory
   64.11    val is_reported_generic: Context.generic -> Position.T -> bool
   64.12 @@ -28,21 +30,25 @@
   64.13  
   64.14  structure Data = Generic_Data
   64.15  (
   64.16 -  type T = bool option;
   64.17 -  val empty: T = NONE;
   64.18 +  type T = bool option * bool option;  (*really, visible*)
   64.19 +  val empty: T = (NONE, NONE);
   64.20    val extend = I;
   64.21 -  fun merge (x, y): T = if is_some x then x else y;
   64.22 +  fun merge ((a, b), (a', b')) : T = (merge_options (a, a'), merge_options (b, b'));
   64.23  );
   64.24  
   64.25 -val is_visible_generic = the_default true o Data.get;
   64.26 +val is_visible_generic = the_default true o snd o Data.get;
   64.27  val is_visible = is_visible_generic o Context.Proof;
   64.28  val is_visible_global = is_visible_generic o Context.Theory;
   64.29  
   64.30 -val set_visible = Context.proof_map o Data.put o SOME;
   64.31 -val set_visible_global = Context.theory_map o Data.put o SOME;
   64.32 +val set_visible = Context.proof_map o Data.map o apsnd o K o SOME;
   64.33 +val set_visible_global = Context.theory_map o Data.map o apsnd o K o SOME;
   64.34  
   64.35 -val restore_visible = set_visible o is_visible;
   64.36 -val restore_visible_global = set_visible_global o is_visible_global;
   64.37 +val is_really = the_default true o fst o Data.get o Context.Proof;
   64.38 +fun is_really_visible ctxt = is_really ctxt andalso is_visible ctxt;
   64.39 +val not_really = Context.proof_map (Data.map (apfst (K (SOME false))));
   64.40 +
   64.41 +val restore_visible = Context.proof_map o Data.put o Data.get o Context.Proof;
   64.42 +val restore_visible_global = Context.theory_map o Data.put o Data.get o Context.Theory;
   64.43  
   64.44  fun is_reported_generic context pos = is_visible_generic context andalso Position.is_reported pos;
   64.45  fun is_reported ctxt pos = is_visible ctxt andalso Position.is_reported pos;
    65.1 --- a/src/Pure/library.ML	Sun Aug 10 14:31:06 2014 +0200
    65.2 +++ b/src/Pure/library.ML	Sun Aug 10 14:34:43 2014 +0200
    65.3 @@ -266,6 +266,7 @@
    65.4  fun error msg = raise ERROR msg;
    65.5  
    65.6  fun cat_error "" msg = error msg
    65.7 +  | cat_error msg "" = error msg
    65.8    | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
    65.9  
   65.10  fun assert_all pred list msg =
    66.1 --- a/src/Pure/library.scala	Sun Aug 10 14:31:06 2014 +0200
    66.2 +++ b/src/Pure/library.scala	Sun Aug 10 14:34:43 2014 +0200
    66.3 @@ -25,6 +25,7 @@
    66.4  
    66.5    def cat_message(msg1: String, msg2: String): String =
    66.6      if (msg1 == "") msg2
    66.7 +    else if (msg2 == "") msg1
    66.8      else msg1 + "\n" + msg2
    66.9  
   66.10    def cat_error(msg1: String, msg2: String): Nothing =
    67.1 --- a/src/Pure/raw_simplifier.ML	Sun Aug 10 14:31:06 2014 +0200
    67.2 +++ b/src/Pure/raw_simplifier.ML	Sun Aug 10 14:34:43 2014 +0200
    67.3 @@ -385,7 +385,7 @@
    67.4      val thy' = Proof_Context.theory_of ctxt';
    67.5    in Context.theory_map (Simpset.map (K (simpset_of ctxt'))) thy' end;
    67.6  
    67.7 -fun map_ss f = Context.mapping (map_theory_simpset f) f;
    67.8 +fun map_ss f = Context.mapping (map_theory_simpset (f o Context_Position.not_really)) f;
    67.9  
   67.10  val clear_simpset =
   67.11    map_simpset (fn Simpset ({depth, ...}, {mk_rews, termless, subgoal_tac, solvers, ...}) =>
   67.12 @@ -428,7 +428,7 @@
   67.13  val simp_trace = Config.bool simp_trace_raw;
   67.14  
   67.15  fun cond_warning ctxt msg =
   67.16 -  if Context_Position.is_visible ctxt then warning (msg ()) else ();
   67.17 +  if Context_Position.is_really_visible ctxt then warning (msg ()) else ();
   67.18  
   67.19  fun cond_tracing' ctxt flag msg =
   67.20    if Config.get ctxt flag then
   67.21 @@ -593,6 +593,7 @@
   67.22  fun add_simp thm ctxt = ctxt addsimps [thm];
   67.23  fun del_simp thm ctxt = ctxt delsimps [thm];
   67.24  
   67.25 +
   67.26  (* congs *)
   67.27  
   67.28  local
    68.1 --- a/src/Sequents/prover.ML	Sun Aug 10 14:31:06 2014 +0200
    68.2 +++ b/src/Sequents/prover.ML	Sun Aug 10 14:34:43 2014 +0200
    68.3 @@ -78,11 +78,13 @@
    68.4    Pack (rules |> which (fn ths =>
    68.5      if member Thm.eq_thm_prop ths th then
    68.6        let
    68.7 -        val ctxt = Context.proof_of context;
    68.8          val _ =
    68.9 -          if Context_Position.is_visible ctxt then
   68.10 -            warning ("Ignoring duplicate theorems:\n" ^ Display.string_of_thm ctxt th)
   68.11 -          else ();
   68.12 +          (case context of
   68.13 +            Context.Proof ctxt =>
   68.14 +              if Context_Position.is_really_visible ctxt then
   68.15 +                warning ("Ignoring duplicate theorems:\n" ^ Display.string_of_thm ctxt th)
   68.16 +              else ()
   68.17 +          | _ => ());
   68.18        in ths end
   68.19      else sort_rules (th :: ths))));
   68.20  
    69.1 --- a/src/Tools/Code/lib/Tools/codegen	Sun Aug 10 14:31:06 2014 +0200
    69.2 +++ b/src/Tools/Code/lib/Tools/codegen	Sun Aug 10 14:34:43 2014 +0200
    69.3 @@ -50,8 +50,10 @@
    69.4  
    69.5  ## invoke code generation
    69.6  
    69.7 -FORMAL_CMD="Toplevel.program (fn () => (use_thy thyname; ML_Context.eval_text_in \
    69.8 -  (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd)) \
    69.9 +FORMAL_CMD="Runtime.toplevel_program (fn () => (use_thy thyname; ML_Context.eval_source_in \
   69.10 +    (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) \
   69.11 +    ML_Compiler.flags \
   69.12 +    {delimited=true, text=ml_cmd, pos=Position.none})) \
   69.13    handle _ => exit 1;"
   69.14  
   69.15  ACTUAL_CMD="val thyname = \"$THYNAME\"; \
    70.1 --- a/src/Tools/jEdit/etc/options	Sun Aug 10 14:31:06 2014 +0200
    70.2 +++ b/src/Tools/jEdit/etc/options	Sun Aug 10 14:34:43 2014 +0200
    70.3 @@ -42,6 +42,12 @@
    70.4  public option jedit_completion : bool = true
    70.5    -- "enable completion popup"
    70.6  
    70.7 +public option jedit_completion_select_enter : bool = false
    70.8 +  -- "select completion item via ENTER"
    70.9 +
   70.10 +public option jedit_completion_select_tab : bool = true
   70.11 +  -- "select completion item via TAB"
   70.12 +
   70.13  public option jedit_completion_context : bool = true
   70.14    -- "use semantic language context for completion"
   70.15  
    71.1 --- a/src/Tools/jEdit/src/active.scala	Sun Aug 10 14:31:06 2014 +0200
    71.2 +++ b/src/Tools/jEdit/src/active.scala	Sun Aug 10 14:34:43 2014 +0200
    71.3 @@ -48,8 +48,14 @@
    71.4                    GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
    71.5                  }
    71.6  
    71.7 -              case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, _), _) =>
    71.8 +              case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
    71.9 +                val link =
   71.10 +                  props match {
   71.11 +                    case Position.Id(id) => PIDE.editor.hyperlink_command_id(snapshot, id)
   71.12 +                    case _ => None
   71.13 +                  }
   71.14                  GUI_Thread.later {
   71.15 +                  link.foreach(_.follow(view))
   71.16                    view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
   71.17                  }
   71.18  
    72.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Sun Aug 10 14:31:06 2014 +0200
    72.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Sun Aug 10 14:34:43 2014 +0200
    72.3 @@ -702,7 +702,10 @@
    72.4          {
    72.5            if (!e.isConsumed) {
    72.6              e.getKeyCode match {
    72.7 -              case KeyEvent.VK_TAB =>
    72.8 +              case KeyEvent.VK_ENTER if PIDE.options.bool("jedit_completion_select_enter") =>
    72.9 +                if (complete_selected()) e.consume
   72.10 +                hide_popup()
   72.11 +              case KeyEvent.VK_TAB if PIDE.options.bool("jedit_completion_select_tab") =>
   72.12                  if (complete_selected()) e.consume
   72.13                  hide_popup()
   72.14                case KeyEvent.VK_ESCAPE =>
    73.1 --- a/src/Tools/jEdit/src/isabelle.scala	Sun Aug 10 14:31:06 2014 +0200
    73.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Sun Aug 10 14:34:43 2014 +0200
    73.3 @@ -232,8 +232,8 @@
    73.4      s: String)
    73.5    {
    73.6      if (!snapshot.is_outdated) {
    73.7 -      snapshot.state.find_command(snapshot.version, id) match {
    73.8 -        case Some((node, command)) =>
    73.9 +      (snapshot.state.find_command(snapshot.version, id), PIDE.document_model(buffer)) match {
   73.10 +        case (Some((node, command)), Some(model)) if command.node_name == model.node_name =>
   73.11            node.command_start(command) match {
   73.12              case Some(start) =>
   73.13                JEdit_Lib.buffer_edit(buffer) {
   73.14 @@ -248,7 +248,7 @@
   73.15                }
   73.16              case None =>
   73.17            }
   73.18 -        case None =>
   73.19 +        case _ =>
   73.20        }
   73.21      }
   73.22    }
    74.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Aug 10 14:31:06 2014 +0200
    74.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Aug 10 14:34:43 2014 +0200
    74.3 @@ -110,16 +110,16 @@
    74.4  
    74.5    /* overlays */
    74.6  
    74.7 -  private var overlays = Document.Overlays.empty
    74.8 +  private val overlays = Synchronized(Document.Overlays.empty)
    74.9  
   74.10    override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
   74.11 -    synchronized { overlays(name) }
   74.12 +    overlays.value(name)
   74.13  
   74.14    override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
   74.15 -    synchronized { overlays = overlays.insert(command, fn, args) }
   74.16 +    overlays.change(_.insert(command, fn, args))
   74.17  
   74.18    override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
   74.19 -    synchronized { overlays = overlays.remove(command, fn, args) }
   74.20 +    overlays.change(_.remove(command, fn, args))
   74.21  
   74.22  
   74.23    /* navigation */
   74.24 @@ -246,7 +246,7 @@
   74.25    def hyperlink_command_id(
   74.26      snapshot: Document.Snapshot,
   74.27      id: Document_ID.Generic,
   74.28 -    offset: Symbol.Offset): Option[Hyperlink] =
   74.29 +    offset: Symbol.Offset = 0): Option[Hyperlink] =
   74.30    {
   74.31      snapshot.state.find_command(snapshot.version, id) match {
   74.32        case Some((node, command)) => hyperlink_command(snapshot, command, offset)
    75.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Aug 10 14:31:06 2014 +0200
    75.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Aug 10 14:34:43 2014 +0200
    75.3 @@ -295,7 +295,7 @@
    75.4        def string_width(s: String): Double =
    75.5          painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
    75.6  
    75.7 -      val unit = string_width(Pretty.space)
    75.8 +      val unit = string_width(Pretty.space) max 1.0
    75.9        val average = string_width("mix") / (3 * unit)
   75.10        def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
   75.11      }
    76.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Sun Aug 10 14:31:06 2014 +0200
    76.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Sun Aug 10 14:34:43 2014 +0200
    76.3 @@ -49,7 +49,8 @@
    76.4    override def append(dir: String, source_path: Path): String =
    76.5    {
    76.6      val path = source_path.expand
    76.7 -    if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path)
    76.8 +    if (dir == "" || path.is_absolute)
    76.9 +      MiscUtilities.resolveSymlinks(Isabelle_System.platform_path(path))
   76.10      else if (path.is_current) dir
   76.11      else {
   76.12        val vfs = VFSManager.getVFSForPath(dir)
    77.1 --- a/src/Tools/jEdit/src/monitor_dockable.scala	Sun Aug 10 14:31:06 2014 +0200
    77.2 +++ b/src/Tools/jEdit/src/monitor_dockable.scala	Sun Aug 10 14:34:43 2014 +0200
    77.3 @@ -1,7 +1,7 @@
    77.4  /*  Title:      Tools/jEdit/src/monitor_dockable.scala
    77.5      Author:     Makarius
    77.6  
    77.7 -Monitor for runtime statistics.
    77.8 +Monitor for ML statistics.
    77.9  */
   77.10  
   77.11  package isabelle.jedit
   77.12 @@ -9,7 +9,10 @@
   77.13  
   77.14  import isabelle._
   77.15  
   77.16 -import scala.swing.{TextArea, ScrollPane, Component}
   77.17 +import java.awt.BorderLayout
   77.18 +
   77.19 +import scala.swing.{TextArea, ScrollPane, Component, ComboBox, Button}
   77.20 +import scala.swing.event.{SelectionChanged, ButtonClicked}
   77.21  
   77.22  import org.jfree.chart.ChartPanel
   77.23  import org.jfree.data.xy.XYSeriesCollection
   77.24 @@ -24,16 +27,51 @@
   77.25  
   77.26    /* chart data -- owned by GUI thread */
   77.27  
   77.28 +  private var data_name = ML_Statistics.standard_fields(0)._1
   77.29    private val chart = ML_Statistics.empty.chart(null, Nil)
   77.30    private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
   77.31  
   77.32 -  private val delay_update =
   77.33 -    GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) {
   77.34 -      ML_Statistics("", rev_stats.value.reverse)
   77.35 -        .update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields
   77.36 +  private def update_chart: Unit =
   77.37 +    ML_Statistics.standard_fields.find(_._1 == data_name) match {
   77.38 +      case None =>
   77.39 +      case Some((_, fields)) =>
   77.40 +        ML_Statistics("", rev_stats.value.reverse).update_data(data, fields)
   77.41      }
   77.42  
   77.43 +  private val delay_update =
   77.44 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { update_chart }
   77.45 +
   77.46 +
   77.47 +  /* controls */
   77.48 +
   77.49 +  private val select_data = new ComboBox[String](
   77.50 +    ML_Statistics.standard_fields.map(_._1))
   77.51 +  {
   77.52 +    tooltip = "Select visualized data collection"
   77.53 +    listenTo(selection)
   77.54 +    reactions += {
   77.55 +      case SelectionChanged(_) =>
   77.56 +        data_name = selection.item
   77.57 +        update_chart
   77.58 +    }
   77.59 +  }
   77.60 +
   77.61 +  val reset_data = new Button("Reset") {
   77.62 +    tooltip = "Reset accumulated data"
   77.63 +    reactions += {
   77.64 +      case ButtonClicked(_) =>
   77.65 +        rev_stats.change(_ => Nil)
   77.66 +        update_chart
   77.67 +    }
   77.68 +  }
   77.69 +
   77.70 +  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(select_data, reset_data)
   77.71 +
   77.72 +
   77.73 +  /* layout */
   77.74 +
   77.75    set_content(new ChartPanel(chart))
   77.76 +  add(controls.peer, BorderLayout.NORTH)
   77.77  
   77.78  
   77.79    /* main */
    78.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Aug 10 14:31:06 2014 +0200
    78.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Aug 10 14:34:43 2014 +0200
    78.3 @@ -391,6 +391,7 @@
    78.4  
    78.5        PIDE.session = new Session(resources) {
    78.6          override def output_delay = PIDE.options.seconds("editor_output_delay")
    78.7 +        override def prune_delay = PIDE.options.seconds("editor_prune_delay")
    78.8          override def reparse_limit = PIDE.options.int("editor_reparse_limit")
    78.9        }
   78.10  
    79.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Aug 10 14:31:06 2014 +0200
    79.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Aug 10 14:34:43 2014 +0200
    79.3 @@ -246,34 +246,32 @@
    79.4      val screen = JEdit_Lib.screen_location(layered, location)
    79.5      val size =
    79.6      {
    79.7 +      val bounds = Rendering.popup_bounds
    79.8 +
    79.9 +      val w_max = layered.getWidth min (screen.bounds.width * bounds).toInt
   79.10 +      val h_max = layered.getHeight min (screen.bounds.height * bounds).toInt
   79.11 +
   79.12        val painter = pretty_text_area.getPainter
   79.13 +      val geometry = JEdit_Lib.window_geometry(tip, painter)
   79.14        val metric = JEdit_Lib.pretty_metric(painter)
   79.15 -      val margin = rendering.tooltip_margin * metric.average
   79.16 +
   79.17 +      val margin =
   79.18 +        ((rendering.tooltip_margin * metric.average) min
   79.19 +          ((w_max - geometry.deco_width) / metric.unit).toInt) max 20
   79.20  
   79.21        val formatted = Pretty.formatted(info.info, margin, metric)
   79.22        val lines =
   79.23          XML.traverse_text(formatted)(0)(
   79.24            (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
   79.25  
   79.26 -      val geometry = JEdit_Lib.window_geometry(tip, tip.pretty_text_area.getPainter)
   79.27 -      val bounds = Rendering.popup_bounds
   79.28 -
   79.29 -      val h0 = layered.getHeight
   79.30 -      val h1 = painter.getFontMetrics.getHeight * (lines + 1) + geometry.deco_height
   79.31 -      val h2 = h0 min (screen.bounds.height * bounds).toInt
   79.32 -      val h = h1 min h2
   79.33 -
   79.34 +      val h = painter.getFontMetrics.getHeight * (lines + 1) + geometry.deco_height
   79.35        val margin1 =
   79.36 -        if (h1 <= h2)
   79.37 +        if (h <= h_max)
   79.38            (0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) })
   79.39          else margin
   79.40 +      val w = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width
   79.41  
   79.42 -      val w0 = layered.getWidth
   79.43 -      val w1 = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width
   79.44 -      val w2 = w0 min (screen.bounds.width * bounds).toInt
   79.45 -      val w = w1 min w2
   79.46 -
   79.47 -      new Dimension(w, h)
   79.48 +      new Dimension(w min w_max, h min h_max)
   79.49      }
   79.50      new Popup(layered, tip, screen.relative(layered, size), size)
   79.51    }
    80.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Aug 10 14:31:06 2014 +0200
    80.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Sun Aug 10 14:34:43 2014 +0200
    80.3 @@ -205,6 +205,7 @@
    80.4    private val mouse_motion_listener = new MouseMotionAdapter {
    80.5      override def mouseDragged(evt: MouseEvent) {
    80.6        robust_body(()) {
    80.7 +        active_reset()
    80.8          Completion_Popup.Text_Area.dismissed(text_area)
    80.9          Pretty_Tooltip.dismiss_descendant(text_area.getPainter)
   80.10        }
    81.1 --- a/src/Tools/jEdit/src/scala_console.scala	Sun Aug 10 14:31:06 2014 +0200
    81.2 +++ b/src/Tools/jEdit/src/scala_console.scala	Sun Aug 10 14:34:43 2014 +0200
    81.3 @@ -201,6 +201,7 @@
    81.4    {
    81.5      out.print(null,
    81.6       "This shell evaluates Isabelle/Scala expressions.\n\n" +
    81.7 +     "The contents of package isabelle and isabelle.jedit are imported.\n" +
    81.8       "The following special toplevel bindings are provided:\n" +
    81.9       "  view    -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
   81.10       "  console -- jEdit Console plugin\n" +
    82.1 --- a/src/ZF/Tools/datatype_package.ML	Sun Aug 10 14:31:06 2014 +0200
    82.2 +++ b/src/ZF/Tools/datatype_package.ML	Sun Aug 10 14:34:43 2014 +0200
    82.3 @@ -51,9 +51,9 @@
    82.4    FIXME: could insert all constant set expressions, e.g. nat->nat.*)
    82.5  fun data_domain co (rec_tms, con_ty_lists) =
    82.6      let val rec_hds = map head_of rec_tms
    82.7 -        val dummy = assert_all is_Const rec_hds
    82.8 -          (fn t => "Datatype set not previously declared as constant: " ^
    82.9 -                   Syntax.string_of_term_global @{theory IFOL} t);
   82.10 +        val dummy = rec_hds |> forall (fn t => is_Const t orelse
   82.11 +          error ("Datatype set not previously declared as constant: " ^
   82.12 +                   Syntax.string_of_term_global @{theory IFOL} t));
   82.13          val rec_names = (*nat doesn't have to be added*)
   82.14              @{const_name nat} :: map (#1 o dest_Const) rec_hds
   82.15          val u = if co then @{const QUniv.quniv} else @{const Univ.univ}
   82.16 @@ -69,9 +69,9 @@
   82.17  
   82.18    val rec_hds = map head_of rec_tms;
   82.19  
   82.20 -  val dummy = assert_all is_Const rec_hds
   82.21 -          (fn t => "Datatype set not previously declared as constant: " ^
   82.22 -                   Syntax.string_of_term_global thy t);
   82.23 +  val dummy = rec_hds |> forall (fn t => is_Const t orelse
   82.24 +          error ("Datatype set not previously declared as constant: " ^
   82.25 +                   Syntax.string_of_term_global thy t));
   82.26  
   82.27    val rec_names = map (#1 o dest_Const) rec_hds
   82.28    val rec_base_names = map Long_Name.base_name rec_names
    83.1 --- a/src/ZF/Tools/inductive_package.ML	Sun Aug 10 14:31:06 2014 +0200
    83.2 +++ b/src/ZF/Tools/inductive_package.ML	Sun Aug 10 14:34:43 2014 +0200
    83.3 @@ -69,31 +69,31 @@
    83.4    (*recT and rec_params should agree for all mutually recursive components*)
    83.5    val rec_hds = map head_of rec_tms;
    83.6  
    83.7 -  val dummy = assert_all is_Const rec_hds
    83.8 -          (fn t => "Recursive set not previously declared as constant: " ^
    83.9 -                   Syntax.string_of_term ctxt t);
   83.10 +  val dummy = rec_hds |> forall (fn t => is_Const t orelse
   83.11 +      error ("Recursive set not previously declared as constant: " ^
   83.12 +                   Syntax.string_of_term ctxt t));
   83.13  
   83.14    (*Now we know they are all Consts, so get their names, type and params*)
   83.15    val rec_names = map (#1 o dest_Const) rec_hds
   83.16    and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
   83.17  
   83.18    val rec_base_names = map Long_Name.base_name rec_names;
   83.19 -  val dummy = assert_all Symbol_Pos.is_identifier rec_base_names
   83.20 -    (fn a => "Base name of recursive set not an identifier: " ^ a);
   83.21 +  val dummy = rec_base_names |> forall (fn a => Symbol_Pos.is_identifier a orelse
   83.22 +    error ("Base name of recursive set not an identifier: " ^ a));
   83.23  
   83.24    local (*Checking the introduction rules*)
   83.25      val intr_sets = map (#2 o Ind_Syntax.rule_concl_msg thy) intr_tms;
   83.26      fun intr_ok set =
   83.27          case head_of set of Const(a,recT) => member (op =) rec_names a | _ => false;
   83.28    in
   83.29 -    val dummy =  assert_all intr_ok intr_sets
   83.30 -       (fn t => "Conclusion of rule does not name a recursive set: " ^
   83.31 -                Syntax.string_of_term ctxt t);
   83.32 +    val dummy = intr_sets |> forall (fn t => intr_ok t orelse
   83.33 +      error ("Conclusion of rule does not name a recursive set: " ^
   83.34 +                Syntax.string_of_term ctxt t));
   83.35    end;
   83.36  
   83.37 -  val dummy = assert_all is_Free rec_params
   83.38 -      (fn t => "Param in recursion term not a free variable: " ^
   83.39 -               Syntax.string_of_term ctxt t);
   83.40 +  val dummy = rec_params |> forall (fn t => is_Free t orelse
   83.41 +      error ("Param in recursion term not a free variable: " ^
   83.42 +               Syntax.string_of_term ctxt t));
   83.43  
   83.44    (*** Construct the fixedpoint definition ***)
   83.45    val mk_variant = singleton (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] intr_tms));