merged
authorwenzelm
Fri Jan 08 16:19:41 2016 +0100 (2016-01-08)
changeset 62099650399eecf2b
parent 62089 4d38c04957fc
parent 62098 b1b2834bb493
child 62100 7a5754afe170
merged
     1.1 --- a/Admin/lib/Tools/makedist_bundle	Fri Jan 08 15:27:16 2016 +0100
     1.2 +++ b/Admin/lib/Tools/makedist_bundle	Fri Jan 08 16:19:41 2016 +0100
     1.3 @@ -325,6 +325,7 @@
     1.4  
     1.5        find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" \
     1.6          > "contrib/cygwin/isabelle/symlinks"
     1.7 +      find . -type l -exec rm "{}" ";"
     1.8  
     1.9        touch "contrib/cygwin/isabelle/uninitialized"
    1.10      )
     2.1 --- a/CONTRIBUTORS	Fri Jan 08 15:27:16 2016 +0100
     2.2 +++ b/CONTRIBUTORS	Fri Jan 08 16:19:41 2016 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4  For the purposes of the license agreement in the file COPYRIGHT, a
     2.5 -'contributor' is anybody who is listed in this file (CONTRIBUTORS) or
     2.6 -who is listed as an author in one of the source files of this Isabelle
     2.7 -distribution.
     2.8 +'contributor' is anybody who is listed in this file (CONTRIBUTORS) or who is
     2.9 +listed as an author in one of the source files of this Isabelle distribution.
    2.10 +
    2.11  
    2.12  Contributions to Isabelle2016
    2.13  -----------------------------
    2.14 @@ -696,3 +696,5 @@
    2.15  * 2004/2005: Tjark Weber, TUM
    2.16    SAT solver method using zChaff.
    2.17    Improved version of HOL/refute.
    2.18 +
    2.19 +:maxLineLen=78:
     3.1 --- a/NEWS	Fri Jan 08 15:27:16 2016 +0100
     3.2 +++ b/NEWS	Fri Jan 08 16:19:41 2016 +0100
     3.3 @@ -443,12 +443,17 @@
     3.4  
     3.5  * Inductive definitions ('inductive', 'coinductive', etc.) expose
     3.6  low-level facts of the internal construction only if the option
     3.7 -"inductive_defs" is enabled. This refers to the internal predicate
     3.8 +"inductive_internals" is enabled. This refers to the internal predicate
     3.9  definition and its monotonicity result. Rare INCOMPATIBILITY.
    3.10  
    3.11  * Recursive function definitions ('fun', 'function', 'partial_function')
    3.12  expose low-level facts of the internal construction only if the option
    3.13 -"function_defs" is enabled. Rare INCOMPATIBILITY.
    3.14 +"function_internals" is enabled. Rare INCOMPATIBILITY.
    3.15 +
    3.16 +* BNF datatypes ('datatype', 'codatatype', etc.) expose low-level facts
    3.17 +of the internal construction only if the option "bnf_internals" is
    3.18 +enabled. This supersedes the former option "bnf_note_all". Rare
    3.19 +INCOMPATIBILITY.
    3.20  
    3.21  * Combinator to represent case distinction on products is named
    3.22  "case_prod", uniformly, discontinuing any input aliasses. Very popular
    3.23 @@ -563,10 +568,9 @@
    3.24      being defined.
    3.25    - Avoid various internal name clashes (e.g., 'datatype f = f').
    3.26  
    3.27 -* Transfer:
    3.28 -  - new methods for interactive debugging of 'transfer' and
    3.29 -    'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end',
    3.30 -    'transfer_prover_start' and 'transfer_prover_end'.
    3.31 +* Transfer: new methods for interactive debugging of 'transfer' and
    3.32 +'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end',
    3.33 +'transfer_prover_start' and 'transfer_prover_end'.
    3.34  
    3.35  * Division on integers is bootstrapped directly from division on
    3.36  naturals and uses generic numeral algorithm for computations. Slight
    3.37 @@ -646,8 +650,9 @@
    3.38  * Library/Periodic_Fun: a locale that provides convenient lemmas for
    3.39  periodic functions.
    3.40  
    3.41 -* Library/Formal_Power_Series: proper definition of division (with remainder) 
    3.42 -for formal power series; instances for Euclidean Ring and GCD.
    3.43 +* Library/Formal_Power_Series: proper definition of division (with
    3.44 +remainder) for formal power series; instances for Euclidean Ring and
    3.45 +GCD.
    3.46  
    3.47  * HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
    3.48  
     4.1 --- a/src/Doc/Datatypes/Datatypes.thy	Fri Jan 08 15:27:16 2016 +0100
     4.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Fri Jan 08 16:19:41 2016 +0100
     4.3 @@ -693,9 +693,9 @@
     4.4  the line
     4.5  \<close>
     4.6  
     4.7 -    declare [[bnf_note_all]]
     4.8 +    declare [[bnf_internals]]
     4.9  (*<*)
    4.10 -    declare [[bnf_note_all = false]]
    4.11 +    declare [[bnf_internals = false]]
    4.12  (*>*)
    4.13  
    4.14  text \<open>
     5.1 --- a/src/HOL/Complete_Partial_Order.thy	Fri Jan 08 15:27:16 2016 +0100
     5.2 +++ b/src/HOL/Complete_Partial_Order.thy	Fri Jan 08 16:19:41 2016 +0100
     5.3 @@ -87,7 +87,7 @@
     5.4  
     5.5  subsection \<open>Transfinite iteration of a function\<close>
     5.6  
     5.7 -context notes [[inductive_defs]] begin
     5.8 +context notes [[inductive_internals]] begin
     5.9  
    5.10  inductive_set iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set"
    5.11  for f :: "'a \<Rightarrow> 'a"
     6.1 --- a/src/HOL/Finite_Set.thy	Fri Jan 08 15:27:16 2016 +0100
     6.2 +++ b/src/HOL/Finite_Set.thy	Fri Jan 08 16:19:41 2016 +0100
     6.3 @@ -12,7 +12,7 @@
     6.4  subsection \<open>Predicate for finite sets\<close>
     6.5  
     6.6  context
     6.7 -  notes [[inductive_defs]]
     6.8 +  notes [[inductive_internals]]
     6.9  begin
    6.10  
    6.11  inductive finite :: "'a set \<Rightarrow> bool"
     7.1 --- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Fri Jan 08 15:27:16 2016 +0100
     7.2 +++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Fri Jan 08 16:19:41 2016 +0100
     7.3 @@ -65,7 +65,7 @@
     7.4    "s \<cdot> P \<equiv> HLD s aand nxt P"
     7.5  
     7.6  context
     7.7 -  notes [[inductive_defs]]
     7.8 +  notes [[inductive_internals]]
     7.9  begin
    7.10  
    7.11  inductive ev for \<phi> where
    7.12 @@ -594,7 +594,7 @@
    7.13  text \<open>Strong until\<close>
    7.14  
    7.15  context
    7.16 -  notes [[inductive_defs]]
    7.17 +  notes [[inductive_internals]]
    7.18  begin
    7.19  
    7.20  inductive suntil (infix "suntil" 60) for \<phi> \<psi> where
     8.1 --- a/src/HOL/Library/RBT_Impl.thy	Fri Jan 08 15:27:16 2016 +0100
     8.2 +++ b/src/HOL/Library/RBT_Impl.thy	Fri Jan 08 16:19:41 2016 +0100
     8.3 @@ -1758,9 +1758,7 @@
     8.4    Rep_compare Rep_compare_cases Rep_compare_induct Rep_compare_inject Rep_compare_inverse
     8.5    compare.simps compare.exhaust compare.induct compare.rec compare.simps
     8.6    compare.size compare.case_cong compare.case_cong_weak compare.case
     8.7 -  compare.nchotomy compare.split compare.split_asm rec_compare_def
     8.8 -  compare.eq.refl compare.eq.simps
     8.9 -  compare.EQ_def compare.GT_def compare.LT_def
    8.10 +  compare.nchotomy compare.split compare.split_asm compare.eq.refl compare.eq.simps
    8.11    equal_compare_def
    8.12    skip_red.simps skip_red.cases skip_red.induct 
    8.13    skip_black_def
     9.1 --- a/src/HOL/Library/Stream.thy	Fri Jan 08 15:27:16 2016 +0100
     9.2 +++ b/src/HOL/Library/Stream.thy	Fri Jan 08 16:19:41 2016 +0100
     9.3 @@ -69,7 +69,7 @@
     9.4  subsection \<open>set of streams with elements in some fixed set\<close>
     9.5  
     9.6  context
     9.7 -  notes [[inductive_defs]]
     9.8 +  notes [[inductive_internals]]
     9.9  begin
    9.10  
    9.11  coinductive_set
    10.1 --- a/src/HOL/List.thy	Fri Jan 08 15:27:16 2016 +0100
    10.2 +++ b/src/HOL/List.thy	Fri Jan 08 16:19:41 2016 +0100
    10.3 @@ -5586,7 +5586,7 @@
    10.4  begin
    10.5  
    10.6  context
    10.7 -  notes [[inductive_defs]]
    10.8 +  notes [[inductive_internals]]
    10.9  begin
   10.10  
   10.11  inductive lexordp :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    11.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jan 08 15:27:16 2016 +0100
    11.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jan 08 16:19:41 2016 +0100
    11.3 @@ -5976,7 +5976,7 @@
    11.4    (is "?int = convex hull ?points")
    11.5  proof -
    11.6    have One[simp]: "\<And>i. i \<in> Basis \<Longrightarrow> One \<bullet> i = 1"
    11.7 -    by (simp add: One_def inner_setsum_left setsum.If_cases inner_Basis)
    11.8 +    by (simp add: inner_setsum_left setsum.If_cases inner_Basis)
    11.9    have "?int = {x. \<forall>i\<in>Basis. x \<bullet> i \<in> cbox 0 1}"
   11.10      by (auto simp: cbox_def)
   11.11    also have "\<dots> = (\<Sum>i\<in>Basis. (\<lambda>x. x *\<^sub>R i) ` cbox 0 1)"
    12.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Fri Jan 08 15:27:16 2016 +0100
    12.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Fri Jan 08 16:19:41 2016 +0100
    12.3 @@ -887,7 +887,7 @@
    12.4  qed
    12.5  
    12.6  context
    12.7 -  notes [[inductive_defs]]
    12.8 +  notes [[inductive_internals]]
    12.9  begin
   12.10  
   12.11  inductive integrable for M f where
    13.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Fri Jan 08 15:27:16 2016 +0100
    13.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Jan 08 16:19:41 2016 +0100
    13.3 @@ -119,7 +119,7 @@
    13.4    datatype inline_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
    13.5    datatype fact_policy = Dont_Note | Note_Some | Note_All
    13.6  
    13.7 -  val bnf_note_all: bool Config.T
    13.8 +  val bnf_internals: bool Config.T
    13.9    val bnf_timing: bool Config.T
   13.10    val user_policy: fact_policy -> Proof.context -> fact_policy
   13.11    val note_bnf_thms: fact_policy -> (binding -> binding) -> binding -> bnf -> Proof.context ->
   13.12 @@ -725,10 +725,10 @@
   13.13  
   13.14  datatype fact_policy = Dont_Note | Note_Some | Note_All;
   13.15  
   13.16 -val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false);
   13.17 +val bnf_internals = Attrib.setup_config_bool @{binding bnf_internals} (K false);
   13.18  val bnf_timing = Attrib.setup_config_bool @{binding bnf_timing} (K false);
   13.19  
   13.20 -fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy;
   13.21 +fun user_policy policy ctxt = if Config.get ctxt bnf_internals then Note_All else policy;
   13.22  
   13.23  val smart_max_inline_term_size = 25; (*FUDGE*)
   13.24  
    14.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Jan 08 15:27:16 2016 +0100
    14.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Jan 08 16:19:41 2016 +0100
    14.3 @@ -1283,12 +1283,10 @@
    14.4    let
    14.5      val thy = Proof_Context.theory_of lthy0;
    14.6  
    14.7 -    val maybe_conceal_def_binding = Thm.def_binding
    14.8 -      #> not (Config.get lthy0 bnf_note_all) ? Binding.concealed;
    14.9 -
   14.10      val ((cst, (_, def)), (lthy', lthy)) = lthy0
   14.11        |> Local_Theory.open_target |> snd
   14.12 -      |> Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
   14.13 +      |> Local_Theory.define
   14.14 +          ((b, NoSyn), ((Thm.make_def_binding (Config.get lthy0 bnf_internals) b, []), rhs))
   14.15        ||> `Local_Theory.close_target;
   14.16  
   14.17      val phi = Proof_Context.export_morphism lthy lthy';
   14.18 @@ -2201,14 +2199,12 @@
   14.19            map2 (fn k => fn xs => fold_rev Term.lambda xs (ctor $ mk_absumprod ctr_absT abs n k xs))
   14.20              ks xss;
   14.21  
   14.22 -        val maybe_conceal_def_binding = Thm.def_binding
   14.23 -          #> not (Config.get no_defs_lthy bnf_note_all) ? Binding.concealed;
   14.24 -
   14.25          val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
   14.26            |> Local_Theory.open_target |> snd
   14.27            |> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs =>
   14.28 -              Local_Theory.define ((b, mx), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd)
   14.29 -            ctr_bindings ctr_mixfixes ctr_rhss
   14.30 +              Local_Theory.define
   14.31 +                ((b, mx), ((Thm.make_def_binding (Config.get no_defs_lthy bnf_internals) b, []), rhs))
   14.32 +                  #>> apsnd snd) ctr_bindings ctr_mixfixes ctr_rhss
   14.33            ||> `Local_Theory.close_target;
   14.34  
   14.35          val phi = Proof_Context.export_morphism lthy lthy';
    15.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Jan 08 15:27:16 2016 +0100
    15.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Jan 08 16:19:41 2016 +0100
    15.3 @@ -646,7 +646,7 @@
    15.4      val Dss = @{map 3} (uncurry append oo curry swap oo map o nth) livess kill_poss deadss;
    15.5  
    15.6      fun pre_qualify b = Binding.qualify false (Binding.name_of b)
    15.7 -      #> not (Config.get lthy' bnf_note_all) ? Binding.concealed;
    15.8 +      #> not (Config.get lthy' bnf_internals) ? Binding.concealed;
    15.9  
   15.10      val ((pre_bnfs, (deadss, absT_infos)), lthy'') =
   15.11        @{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
    16.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Jan 08 15:27:16 2016 +0100
    16.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Jan 08 16:19:41 2016 +0100
    16.3 @@ -66,7 +66,7 @@
    16.4      val m = live - n; (*passive, if 0 don't generate a new BNF*)
    16.5      val ls = 1 upto m;
    16.6  
    16.7 -    val note_all = Config.get lthy bnf_note_all;
    16.8 +    val internals = Config.get lthy bnf_internals;
    16.9      val b_names = map Binding.name_of bs;
   16.10      val b_name = mk_common_name b_names;
   16.11      val b = Binding.name b_name;
   16.12 @@ -76,7 +76,7 @@
   16.13      fun mk_internal_b name = mk_internal_of_b name b;
   16.14      fun mk_internal_bs name = map (mk_internal_of_b name) bs;
   16.15      val external_bs = map2 (Binding.prefix false) b_names bs
   16.16 -      |> not note_all ? map Binding.concealed;
   16.17 +      |> not internals ? map Binding.concealed;
   16.18  
   16.19      val deads = fold (union (op =)) Dss resDs;
   16.20      val names_lthy = fold Variable.declare_typ deads lthy;
   16.21 @@ -2680,7 +2680,7 @@
   16.22            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
   16.23          bs thmss);
   16.24  
   16.25 -    val lthy' = lthy |> note_all ? snd o Local_Theory.notes (common_notes @ notes @ Jbnf_notes);
   16.26 +    val lthy' = lthy |> internals ? snd o Local_Theory.notes (common_notes @ notes @ Jbnf_notes);
   16.27  
   16.28      val fp_res =
   16.29        {Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_un_folds = unfolds,
    17.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Fri Jan 08 15:27:16 2016 +0100
    17.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Fri Jan 08 16:19:41 2016 +0100
    17.3 @@ -36,7 +36,7 @@
    17.4      val ks = 1 upto n;
    17.5      val m = live - n; (*passive, if 0 don't generate a new BNF*)
    17.6  
    17.7 -    val note_all = Config.get lthy bnf_note_all;
    17.8 +    val internals = Config.get lthy bnf_internals;
    17.9      val b_names = map Binding.name_of bs;
   17.10      val b_name = mk_common_name b_names;
   17.11      val b = Binding.name b_name;
   17.12 @@ -46,7 +46,7 @@
   17.13      fun mk_internal_b name = mk_internal_of_b name b;
   17.14      fun mk_internal_bs name = map (mk_internal_of_b name) bs;
   17.15      val external_bs = map2 (Binding.prefix false) b_names bs
   17.16 -      |> not note_all ? map Binding.concealed;
   17.17 +      |> not internals ? map Binding.concealed;
   17.18  
   17.19      val deads = fold (union (op =)) Dss resDs;
   17.20      val names_lthy = fold Variable.declare_typ deads lthy;
   17.21 @@ -1940,7 +1940,7 @@
   17.22            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
   17.23          bs thmss);
   17.24  
   17.25 -    val lthy' = lthy |> note_all ? snd o Local_Theory.notes (common_notes @ notes @ Ibnf_notes);
   17.26 +    val lthy' = lthy |> internals ? snd o Local_Theory.notes (common_notes @ notes @ Ibnf_notes);
   17.27  
   17.28      val fp_res =
   17.29        {Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_folds = folds,
    18.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Jan 08 15:27:16 2016 +0100
    18.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Jan 08 16:19:41 2016 +0100
    18.3 @@ -200,7 +200,7 @@
    18.4          #>> (fn args => fold_rev Term.lambda fs (Term.list_comb (substCnatT recx, args)));
    18.5  
    18.6        val maybe_conceal_def_binding = Thm.def_binding
    18.7 -        #> not (Config.get lthy0 bnf_note_all) ? Binding.concealed;
    18.8 +        #> not (Config.get lthy0 bnf_internals) ? Binding.concealed;
    18.9  
   18.10        val (size_rhss, nested_size_gen_o_mapss) = fold_map mk_size_rhs recs [];
   18.11        val size_Ts = map fastype_of size_rhss;
    19.1 --- a/src/HOL/Tools/Function/function_core.ML	Fri Jan 08 15:27:16 2016 +0100
    19.2 +++ b/src/HOL/Tools/Function/function_core.ML	Fri Jan 08 16:19:41 2016 +0100
    19.3 @@ -499,7 +499,7 @@
    19.4          $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
    19.5        |> Syntax.check_term lthy
    19.6      val def_binding =
    19.7 -      if Config.get lthy function_defs then (Binding.name fdefname, [])
    19.8 +      if Config.get lthy function_internals then (Binding.name fdefname, [])
    19.9        else Attrib.empty_binding
   19.10    in
   19.11      Local_Theory.define
    20.1 --- a/src/HOL/Tools/Function/function_lib.ML	Fri Jan 08 15:27:16 2016 +0100
    20.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Fri Jan 08 16:19:41 2016 +0100
    20.3 @@ -7,7 +7,7 @@
    20.4  
    20.5  signature FUNCTION_LIB =
    20.6  sig
    20.7 -  val function_defs: bool Config.T
    20.8 +  val function_internals: bool Config.T
    20.9  
   20.10    val plural: string -> string -> 'a list -> string
   20.11  
   20.12 @@ -32,7 +32,7 @@
   20.13  structure Function_Lib: FUNCTION_LIB =
   20.14  struct
   20.15  
   20.16 -val function_defs = Attrib.setup_config_bool @{binding function_defs} (K false)
   20.17 +val function_internals = Attrib.setup_config_bool @{binding function_internals} (K false)
   20.18  
   20.19  
   20.20  (* "The variable" ^ plural " is" "s are" vs *)
    21.1 --- a/src/HOL/Tools/Function/mutual.ML	Fri Jan 08 15:27:16 2016 +0100
    21.2 +++ b/src/HOL/Tools/Function/mutual.ML	Fri Jan 08 16:19:41 2016 +0100
    21.3 @@ -129,7 +129,7 @@
    21.4      fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
    21.5        let
    21.6          val def_binding =
    21.7 -          if Config.get lthy function_defs then (Binding.name (Thm.def_name fname), [])
    21.8 +          if Config.get lthy function_internals then (Binding.name (Thm.def_name fname), [])
    21.9            else Attrib.empty_binding
   21.10          val ((f, (_, f_defthm)), lthy') =
   21.11            Local_Theory.define
    22.1 --- a/src/HOL/Tools/Function/partial_function.ML	Fri Jan 08 15:27:16 2016 +0100
    22.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Fri Jan 08 16:19:41 2016 +0100
    22.3 @@ -257,7 +257,8 @@
    22.4  
    22.5      val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc);
    22.6      val f_def_binding =
    22.7 -      if Config.get lthy Function_Lib.function_defs then (Binding.name (Thm.def_name fname), [])
    22.8 +      if Config.get lthy Function_Lib.function_internals
    22.9 +      then (Binding.name (Thm.def_name fname), [])
   22.10        else Attrib.empty_binding;
   22.11      val ((f, (_, f_def)), lthy') = Local_Theory.define
   22.12        ((f_binding, mixfix), (f_def_binding, f_def_rhs)) lthy;
    23.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Jan 08 15:27:16 2016 +0100
    23.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Jan 08 16:19:41 2016 +0100
    23.3 @@ -23,7 +23,7 @@
    23.4  
    23.5    val fact_of_ref : Proof.context -> Keyword.keywords -> thm list -> status Termtab.table ->
    23.6      Facts.ref * Token.src list -> ((string * stature) * thm) list
    23.7 -  val backquote_thm : Proof.context -> thm -> string
    23.8 +  val cartouche_thm : Proof.context -> thm -> string
    23.9    val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
   23.10    val clasimpset_rule_table_of : Proof.context -> status Termtab.table
   23.11    val build_name_tables : (thm -> string) -> ('a * thm) list ->
   23.12 @@ -81,11 +81,6 @@
   23.13    | explode_interval max (Facts.From i) = i upto i + max - 1
   23.14    | explode_interval _ (Facts.Single i) = [i]
   23.15  
   23.16 -val backquote = enclose "\<open>" "\<close>"
   23.17 -
   23.18 -(* unfolding these can yield really huge terms *)
   23.19 -val risky_defs = @{thms Bit0_def Bit1_def}
   23.20 -
   23.21  fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
   23.22  
   23.23  fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
   23.24 @@ -168,7 +163,7 @@
   23.25  
   23.26      fun nth_name j =
   23.27        (case xref of
   23.28 -        Facts.Fact s => backquote (simplify_spaces (YXML.content_of s)) ^ bracket
   23.29 +        Facts.Fact s => cartouche (simplify_spaces (YXML.content_of s)) ^ bracket
   23.30        | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
   23.31        | Facts.Named ((name, _), NONE) => make_name keywords (length ths > 1) (j + 1) name ^ bracket
   23.32        | Facts.Named ((name, _), SOME intervals) =>
   23.33 @@ -301,8 +296,8 @@
   23.34      (Term.add_vars t [] |> sort_by (fst o fst))
   23.35    |> fst
   23.36  
   23.37 -fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote
   23.38 -fun backquote_thm ctxt = backquote_term ctxt o Thm.prop_of
   23.39 +fun cartouche_term ctxt = close_form #> hackish_string_of_term ctxt #> cartouche
   23.40 +fun cartouche_thm ctxt = cartouche_term ctxt o Thm.prop_of
   23.41  
   23.42  (* TODO: rewrite to use nets and/or to reuse existing data structures *)
   23.43  fun clasimpset_rule_table_of ctxt =
   23.44 @@ -324,7 +319,6 @@
   23.45          val (rec_defs, nonrec_defs) = specs
   23.46            |> filter (curry (op =) Spec_Rules.Equational o fst)
   23.47            |> maps (snd o snd)
   23.48 -          |> filter_out (member Thm.eq_thm_prop risky_defs)
   23.49            |> List.partition (is_rec_def o Thm.prop_of)
   23.50          val spec_intros = specs
   23.51            |> filter (member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] o fst)
   23.52 @@ -509,7 +503,7 @@
   23.53                     let
   23.54                       fun get_name () =
   23.55                         if name0 = "" orelse name0 = local_thisN then
   23.56 -                         backquote_thm ctxt th
   23.57 +                         cartouche_thm ctxt th
   23.58                         else
   23.59                           let val short_name = Facts.extern ctxt facts name0 in
   23.60                             if check_thms short_name then
    24.1 --- a/src/HOL/Tools/inductive.ML	Fri Jan 08 15:27:16 2016 +0100
    24.2 +++ b/src/HOL/Tools/inductive.ML	Fri Jan 08 16:19:41 2016 +0100
    24.3 @@ -71,7 +71,7 @@
    24.4  signature INDUCTIVE =
    24.5  sig
    24.6    include BASIC_INDUCTIVE
    24.7 -  val inductive_defs: bool Config.T
    24.8 +  val inductive_internals: bool Config.T
    24.9    val select_disj_tac: Proof.context -> int -> int -> int -> tactic
   24.10    type add_ind_def =
   24.11      inductive_flags ->
   24.12 @@ -122,7 +122,7 @@
   24.13  
   24.14  (** misc utilities **)
   24.15  
   24.16 -val inductive_defs = Attrib.setup_config_bool @{binding inductive_defs} (K false);
   24.17 +val inductive_internals = Attrib.setup_config_bool @{binding inductive_internals} (K false);
   24.18  
   24.19  fun message quiet_mode s = if quiet_mode then () else writeln s;
   24.20  
   24.21 @@ -849,16 +849,13 @@
   24.22        else alt_name;
   24.23      val rec_name = Binding.name_of rec_binding;
   24.24  
   24.25 -    val inductive_defs = Config.get lthy inductive_defs;
   24.26 -    fun cond_def_binding b =
   24.27 -      if inductive_defs then Binding.reset_pos (Thm.def_binding b)
   24.28 -      else Binding.empty;
   24.29 +    val internals = Config.get lthy inductive_internals;
   24.30  
   24.31      val ((rec_const, (_, fp_def)), lthy') = lthy
   24.32        |> is_auxiliary ? Proof_Context.concealed
   24.33        |> Local_Theory.define
   24.34          ((rec_binding, case cnames_syn of [(_, mx)] => mx | _ => NoSyn),
   24.35 -         ((cond_def_binding rec_binding, @{attributes [nitpick_unfold]}),
   24.36 +         ((Thm.make_def_binding internals rec_binding, @{attributes [nitpick_unfold]}),
   24.37             fold_rev lambda params
   24.38               (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
   24.39        ||> Proof_Context.restore_naming lthy;
   24.40 @@ -874,7 +871,7 @@
   24.41                map Free (Variable.variant_frees lthy' intr_ts (mk_names "x" (length Ts) ~~ Ts));
   24.42            in
   24.43              ((b, mx),
   24.44 -              ((cond_def_binding b, []), fold_rev lambda (params @ xs)
   24.45 +              ((Thm.make_def_binding internals b, []), fold_rev lambda (params @ xs)
   24.46                  (list_comb (rec_const, params @ make_bool_args' bs i @
   24.47                    make_args argTs (xs ~~ Ts)))))
   24.48            end) (cnames_syn ~~ cs)
   24.49 @@ -887,7 +884,7 @@
   24.50      val mono = prove_mono quiet_mode skip_mono predT fp_fun monos ctxt'';
   24.51      val (_, lthy''') = lthy''
   24.52        |> Local_Theory.note
   24.53 -        ((if inductive_defs
   24.54 +        ((if internals
   24.55            then Binding.qualify true rec_name (Binding.name "mono")
   24.56            else Binding.empty, []),
   24.57            Proof_Context.export ctxt'' lthy'' [mono]);
    25.1 --- a/src/HOL/Transitive_Closure.thy	Fri Jan 08 15:27:16 2016 +0100
    25.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Jan 08 16:19:41 2016 +0100
    25.3 @@ -21,7 +21,7 @@
    25.4  \<close>
    25.5  
    25.6  context
    25.7 -  notes [[inductive_defs]]
    25.8 +  notes [[inductive_internals]]
    25.9  begin
   25.10  
   25.11  inductive_set rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  ("(_\<^sup>*)" [1000] 999)
    26.1 --- a/src/Pure/General/pretty.ML	Fri Jan 08 15:27:16 2016 +0100
    26.2 +++ b/src/Pure/General/pretty.ML	Fri Jan 08 16:19:41 2016 +0100
    26.3 @@ -45,7 +45,6 @@
    26.4    val paragraph: T list -> T
    26.5    val para: string -> T
    26.6    val quote: T -> T
    26.7 -  val backquote: T -> T
    26.8    val cartouche: T -> T
    26.9    val separate: string -> T list -> T list
   26.10    val commas: T list -> T list
   26.11 @@ -168,7 +167,6 @@
   26.12  val para = paragraph o text;
   26.13  
   26.14  fun quote prt = blk (1, [str "\"", prt, str "\""]);
   26.15 -fun backquote prt = blk (1, [str "`", prt, str "`"]);
   26.16  fun cartouche prt = blk (1, [str "\\<open>", prt, str "\\<close>"]);
   26.17  
   26.18  fun separate sep prts =
    27.1 --- a/src/Pure/Isar/bundle.ML	Fri Jan 08 15:27:16 2016 +0100
    27.2 +++ b/src/Pure/Isar/bundle.ML	Fri Jan 08 16:19:41 2016 +0100
    27.3 @@ -124,7 +124,7 @@
    27.4  
    27.5  fun print_bundles verbose ctxt =
    27.6    let
    27.7 -    val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt;
    27.8 +    val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
    27.9  
   27.10      fun prt_fact (ths, []) = map prt_thm ths
   27.11        | prt_fact (ths, atts) = Pretty.enclose "(" ")"
    28.1 --- a/src/Pure/Isar/element.ML	Fri Jan 08 15:27:16 2016 +0100
    28.2 +++ b/src/Pure/Isar/element.ML	Fri Jan 08 16:19:41 2016 +0100
    28.3 @@ -152,7 +152,7 @@
    28.4    let
    28.5      val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
    28.6      val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
    28.7 -    val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt;
    28.8 +    val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
    28.9  
   28.10      fun prt_binding (b, atts) =
   28.11        Attrib.pretty_binding ctxt (b, if show_attribs then atts else []);
    29.1 --- a/src/Pure/Isar/token.ML	Fri Jan 08 15:27:16 2016 +0100
    29.2 +++ b/src/Pure/Isar/token.ML	Fri Jan 08 16:19:41 2016 +0100
    29.3 @@ -471,7 +471,7 @@
    29.4    | SOME (Typ T) => Syntax.pretty_typ ctxt T
    29.5    | SOME (Term t) => Syntax.pretty_term ctxt t
    29.6    | SOME (Fact (_, ths)) =>
    29.7 -      Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Thm.pretty_thm ctxt) ths))
    29.8 +      Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.cartouche o Thm.pretty_thm ctxt) ths))
    29.9    | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok));
   29.10  
   29.11  
    30.1 --- a/src/Pure/more_thm.ML	Fri Jan 08 15:27:16 2016 +0100
    30.2 +++ b/src/Pure/more_thm.ML	Fri Jan 08 16:19:41 2016 +0100
    30.3 @@ -92,6 +92,7 @@
    30.4    val def_name_optional: string -> string -> string
    30.5    val def_binding: Binding.binding -> Binding.binding
    30.6    val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding
    30.7 +  val make_def_binding: bool -> Binding.binding -> Binding.binding
    30.8    val has_name_hint: thm -> bool
    30.9    val get_name_hint: thm -> string
   30.10    val put_name_hint: string -> thm -> thm
   30.11 @@ -570,6 +571,9 @@
   30.12  fun def_binding_optional b name =
   30.13    if Binding.is_empty name then def_binding b else name;
   30.14  
   30.15 +fun make_def_binding cond b =
   30.16 +  if cond then Binding.reset_pos (def_binding b) else Binding.empty;
   30.17 +
   30.18  
   30.19  (* unofficial theorem names *)
   30.20  
    31.1 --- a/src/Tools/jEdit/src/document_view.scala	Fri Jan 08 15:27:16 2016 +0100
    31.2 +++ b/src/Tools/jEdit/src/document_view.scala	Fri Jan 08 16:19:41 2016 +0100
    31.3 @@ -256,7 +256,7 @@
    31.4      text_area.getGutter.addExtension(gutter_painter)
    31.5      text_area.addKeyListener(key_listener)
    31.6      text_area.addCaretListener(caret_listener)
    31.7 -    text_area.addLeftOfScrollBar(overview)
    31.8 +    text_area.addLeftOfScrollBar(overview); text_area.revalidate(); text_area.repaint()
    31.9      Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
   31.10        foreach(text_area.addStructureMatcher(_))
   31.11      session.raw_edits += main
   31.12 @@ -271,7 +271,7 @@
   31.13      session.commands_changed -= main
   31.14      Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
   31.15        foreach(text_area.removeStructureMatcher(_))
   31.16 -    text_area.removeLeftOfScrollBar(overview); overview.revoke()
   31.17 +    overview.revoke(); text_area.removeLeftOfScrollBar(overview)
   31.18      text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
   31.19      text_area.removeKeyListener(key_listener)
   31.20      text_area.getGutter.removeExtension(gutter_painter)
    32.1 --- a/src/Tools/jEdit/src/text_overview.scala	Fri Jan 08 15:27:16 2016 +0100
    32.2 +++ b/src/Tools/jEdit/src/text_overview.scala	Fri Jan 08 16:19:41 2016 +0100
    32.3 @@ -82,7 +82,13 @@
    32.4          val rendering = doc_view.get_rendering()
    32.5          val overview = get_overview()
    32.6  
    32.7 -        if (!rendering.snapshot.is_outdated && overview == current_overview) {
    32.8 +        if (rendering.snapshot.is_outdated || overview != current_overview) {
    32.9 +          invoke()
   32.10 +
   32.11 +          gfx.setColor(rendering.outdated_color)
   32.12 +          gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
   32.13 +        }
   32.14 +        else {
   32.15            gfx.setColor(getBackground)
   32.16            gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
   32.17            for ((color, h, h1) <- current_colors) {
   32.18 @@ -90,10 +96,6 @@
   32.19              gfx.fillRect(0, h, getWidth, h1 - h)
   32.20            }
   32.21          }
   32.22 -        else {
   32.23 -          gfx.setColor(rendering.outdated_color)
   32.24 -          gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
   32.25 -        }
   32.26        }
   32.27      }
   32.28    }