--- a/Admin/lib/Tools/makedist_bundle Fri Jan 08 15:27:16 2016 +0100
+++ b/Admin/lib/Tools/makedist_bundle Fri Jan 08 16:19:41 2016 +0100
@@ -325,6 +325,7 @@
find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" \
> "contrib/cygwin/isabelle/symlinks"
+ find . -type l -exec rm "{}" ";"
touch "contrib/cygwin/isabelle/uninitialized"
)
--- a/CONTRIBUTORS Fri Jan 08 15:27:16 2016 +0100
+++ b/CONTRIBUTORS Fri Jan 08 16:19:41 2016 +0100
@@ -1,7 +1,7 @@
For the purposes of the license agreement in the file COPYRIGHT, a
-'contributor' is anybody who is listed in this file (CONTRIBUTORS) or
-who is listed as an author in one of the source files of this Isabelle
-distribution.
+'contributor' is anybody who is listed in this file (CONTRIBUTORS) or who is
+listed as an author in one of the source files of this Isabelle distribution.
+
Contributions to Isabelle2016
-----------------------------
@@ -696,3 +696,5 @@
* 2004/2005: Tjark Weber, TUM
SAT solver method using zChaff.
Improved version of HOL/refute.
+
+:maxLineLen=78:
--- a/NEWS Fri Jan 08 15:27:16 2016 +0100
+++ b/NEWS Fri Jan 08 16:19:41 2016 +0100
@@ -443,12 +443,17 @@
* Inductive definitions ('inductive', 'coinductive', etc.) expose
low-level facts of the internal construction only if the option
-"inductive_defs" is enabled. This refers to the internal predicate
+"inductive_internals" is enabled. This refers to the internal predicate
definition and its monotonicity result. Rare INCOMPATIBILITY.
* Recursive function definitions ('fun', 'function', 'partial_function')
expose low-level facts of the internal construction only if the option
-"function_defs" is enabled. Rare INCOMPATIBILITY.
+"function_internals" is enabled. Rare INCOMPATIBILITY.
+
+* BNF datatypes ('datatype', 'codatatype', etc.) expose low-level facts
+of the internal construction only if the option "bnf_internals" is
+enabled. This supersedes the former option "bnf_note_all". Rare
+INCOMPATIBILITY.
* Combinator to represent case distinction on products is named
"case_prod", uniformly, discontinuing any input aliasses. Very popular
@@ -563,10 +568,9 @@
being defined.
- Avoid various internal name clashes (e.g., 'datatype f = f').
-* Transfer:
- - new methods for interactive debugging of 'transfer' and
- 'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end',
- 'transfer_prover_start' and 'transfer_prover_end'.
+* Transfer: new methods for interactive debugging of 'transfer' and
+'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end',
+'transfer_prover_start' and 'transfer_prover_end'.
* Division on integers is bootstrapped directly from division on
naturals and uses generic numeral algorithm for computations. Slight
@@ -646,8 +650,9 @@
* Library/Periodic_Fun: a locale that provides convenient lemmas for
periodic functions.
-* Library/Formal_Power_Series: proper definition of division (with remainder)
-for formal power series; instances for Euclidean Ring and GCD.
+* Library/Formal_Power_Series: proper definition of division (with
+remainder) for formal power series; instances for Euclidean Ring and
+GCD.
* HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
--- a/src/Doc/Datatypes/Datatypes.thy Fri Jan 08 15:27:16 2016 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Jan 08 16:19:41 2016 +0100
@@ -693,9 +693,9 @@
the line
\<close>
- declare [[bnf_note_all]]
+ declare [[bnf_internals]]
(*<*)
- declare [[bnf_note_all = false]]
+ declare [[bnf_internals = false]]
(*>*)
text \<open>
--- a/src/HOL/Complete_Partial_Order.thy Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Complete_Partial_Order.thy Fri Jan 08 16:19:41 2016 +0100
@@ -87,7 +87,7 @@
subsection \<open>Transfinite iteration of a function\<close>
-context notes [[inductive_defs]] begin
+context notes [[inductive_internals]] begin
inductive_set iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set"
for f :: "'a \<Rightarrow> 'a"
--- a/src/HOL/Finite_Set.thy Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Finite_Set.thy Fri Jan 08 16:19:41 2016 +0100
@@ -12,7 +12,7 @@
subsection \<open>Predicate for finite sets\<close>
context
- notes [[inductive_defs]]
+ notes [[inductive_internals]]
begin
inductive finite :: "'a set \<Rightarrow> bool"
--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Fri Jan 08 16:19:41 2016 +0100
@@ -65,7 +65,7 @@
"s \<cdot> P \<equiv> HLD s aand nxt P"
context
- notes [[inductive_defs]]
+ notes [[inductive_internals]]
begin
inductive ev for \<phi> where
@@ -594,7 +594,7 @@
text \<open>Strong until\<close>
context
- notes [[inductive_defs]]
+ notes [[inductive_internals]]
begin
inductive suntil (infix "suntil" 60) for \<phi> \<psi> where
--- a/src/HOL/Library/RBT_Impl.thy Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Library/RBT_Impl.thy Fri Jan 08 16:19:41 2016 +0100
@@ -1758,9 +1758,7 @@
Rep_compare Rep_compare_cases Rep_compare_induct Rep_compare_inject Rep_compare_inverse
compare.simps compare.exhaust compare.induct compare.rec compare.simps
compare.size compare.case_cong compare.case_cong_weak compare.case
- compare.nchotomy compare.split compare.split_asm rec_compare_def
- compare.eq.refl compare.eq.simps
- compare.EQ_def compare.GT_def compare.LT_def
+ compare.nchotomy compare.split compare.split_asm compare.eq.refl compare.eq.simps
equal_compare_def
skip_red.simps skip_red.cases skip_red.induct
skip_black_def
--- a/src/HOL/Library/Stream.thy Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Library/Stream.thy Fri Jan 08 16:19:41 2016 +0100
@@ -69,7 +69,7 @@
subsection \<open>set of streams with elements in some fixed set\<close>
context
- notes [[inductive_defs]]
+ notes [[inductive_internals]]
begin
coinductive_set
--- a/src/HOL/List.thy Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/List.thy Fri Jan 08 16:19:41 2016 +0100
@@ -5586,7 +5586,7 @@
begin
context
- notes [[inductive_defs]]
+ notes [[inductive_internals]]
begin
inductive lexordp :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jan 08 16:19:41 2016 +0100
@@ -5976,7 +5976,7 @@
(is "?int = convex hull ?points")
proof -
have One[simp]: "\<And>i. i \<in> Basis \<Longrightarrow> One \<bullet> i = 1"
- by (simp add: One_def inner_setsum_left setsum.If_cases inner_Basis)
+ by (simp add: inner_setsum_left setsum.If_cases inner_Basis)
have "?int = {x. \<forall>i\<in>Basis. x \<bullet> i \<in> cbox 0 1}"
by (auto simp: cbox_def)
also have "\<dots> = (\<Sum>i\<in>Basis. (\<lambda>x. x *\<^sub>R i) ` cbox 0 1)"
--- a/src/HOL/Probability/Bochner_Integration.thy Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy Fri Jan 08 16:19:41 2016 +0100
@@ -887,7 +887,7 @@
qed
context
- notes [[inductive_defs]]
+ notes [[inductive_internals]]
begin
inductive integrable for M f where
--- a/src/HOL/Tools/BNF/bnf_def.ML Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Jan 08 16:19:41 2016 +0100
@@ -119,7 +119,7 @@
datatype inline_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
datatype fact_policy = Dont_Note | Note_Some | Note_All
- val bnf_note_all: bool Config.T
+ val bnf_internals: bool Config.T
val bnf_timing: bool Config.T
val user_policy: fact_policy -> Proof.context -> fact_policy
val note_bnf_thms: fact_policy -> (binding -> binding) -> binding -> bnf -> Proof.context ->
@@ -725,10 +725,10 @@
datatype fact_policy = Dont_Note | Note_Some | Note_All;
-val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false);
+val bnf_internals = Attrib.setup_config_bool @{binding bnf_internals} (K false);
val bnf_timing = Attrib.setup_config_bool @{binding bnf_timing} (K false);
-fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy;
+fun user_policy policy ctxt = if Config.get ctxt bnf_internals then Note_All else policy;
val smart_max_inline_term_size = 25; (*FUDGE*)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Jan 08 16:19:41 2016 +0100
@@ -1283,12 +1283,10 @@
let
val thy = Proof_Context.theory_of lthy0;
- val maybe_conceal_def_binding = Thm.def_binding
- #> not (Config.get lthy0 bnf_note_all) ? Binding.concealed;
-
val ((cst, (_, def)), (lthy', lthy)) = lthy0
|> Local_Theory.open_target |> snd
- |> Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
+ |> Local_Theory.define
+ ((b, NoSyn), ((Thm.make_def_binding (Config.get lthy0 bnf_internals) b, []), rhs))
||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy lthy';
@@ -2201,14 +2199,12 @@
map2 (fn k => fn xs => fold_rev Term.lambda xs (ctor $ mk_absumprod ctr_absT abs n k xs))
ks xss;
- val maybe_conceal_def_binding = Thm.def_binding
- #> not (Config.get no_defs_lthy bnf_note_all) ? Binding.concealed;
-
val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
|> Local_Theory.open_target |> snd
|> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs =>
- Local_Theory.define ((b, mx), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd)
- ctr_bindings ctr_mixfixes ctr_rhss
+ Local_Theory.define
+ ((b, mx), ((Thm.make_def_binding (Config.get no_defs_lthy bnf_internals) b, []), rhs))
+ #>> apsnd snd) ctr_bindings ctr_mixfixes ctr_rhss
||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy lthy';
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Jan 08 16:19:41 2016 +0100
@@ -646,7 +646,7 @@
val Dss = @{map 3} (uncurry append oo curry swap oo map o nth) livess kill_poss deadss;
fun pre_qualify b = Binding.qualify false (Binding.name_of b)
- #> not (Config.get lthy' bnf_note_all) ? Binding.concealed;
+ #> not (Config.get lthy' bnf_internals) ? Binding.concealed;
val ((pre_bnfs, (deadss, absT_infos)), lthy'') =
@{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Fri Jan 08 16:19:41 2016 +0100
@@ -66,7 +66,7 @@
val m = live - n; (*passive, if 0 don't generate a new BNF*)
val ls = 1 upto m;
- val note_all = Config.get lthy bnf_note_all;
+ val internals = Config.get lthy bnf_internals;
val b_names = map Binding.name_of bs;
val b_name = mk_common_name b_names;
val b = Binding.name b_name;
@@ -76,7 +76,7 @@
fun mk_internal_b name = mk_internal_of_b name b;
fun mk_internal_bs name = map (mk_internal_of_b name) bs;
val external_bs = map2 (Binding.prefix false) b_names bs
- |> not note_all ? map Binding.concealed;
+ |> not internals ? map Binding.concealed;
val deads = fold (union (op =)) Dss resDs;
val names_lthy = fold Variable.declare_typ deads lthy;
@@ -2680,7 +2680,7 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss);
- val lthy' = lthy |> note_all ? snd o Local_Theory.notes (common_notes @ notes @ Jbnf_notes);
+ val lthy' = lthy |> internals ? snd o Local_Theory.notes (common_notes @ notes @ Jbnf_notes);
val fp_res =
{Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_un_folds = unfolds,
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Fri Jan 08 16:19:41 2016 +0100
@@ -36,7 +36,7 @@
val ks = 1 upto n;
val m = live - n; (*passive, if 0 don't generate a new BNF*)
- val note_all = Config.get lthy bnf_note_all;
+ val internals = Config.get lthy bnf_internals;
val b_names = map Binding.name_of bs;
val b_name = mk_common_name b_names;
val b = Binding.name b_name;
@@ -46,7 +46,7 @@
fun mk_internal_b name = mk_internal_of_b name b;
fun mk_internal_bs name = map (mk_internal_of_b name) bs;
val external_bs = map2 (Binding.prefix false) b_names bs
- |> not note_all ? map Binding.concealed;
+ |> not internals ? map Binding.concealed;
val deads = fold (union (op =)) Dss resDs;
val names_lthy = fold Variable.declare_typ deads lthy;
@@ -1940,7 +1940,7 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss);
- val lthy' = lthy |> note_all ? snd o Local_Theory.notes (common_notes @ notes @ Ibnf_notes);
+ val lthy' = lthy |> internals ? snd o Local_Theory.notes (common_notes @ notes @ Ibnf_notes);
val fp_res =
{Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_folds = folds,
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Jan 08 16:19:41 2016 +0100
@@ -200,7 +200,7 @@
#>> (fn args => fold_rev Term.lambda fs (Term.list_comb (substCnatT recx, args)));
val maybe_conceal_def_binding = Thm.def_binding
- #> not (Config.get lthy0 bnf_note_all) ? Binding.concealed;
+ #> not (Config.get lthy0 bnf_internals) ? Binding.concealed;
val (size_rhss, nested_size_gen_o_mapss) = fold_map mk_size_rhs recs [];
val size_Ts = map fastype_of size_rhss;
--- a/src/HOL/Tools/Function/function_core.ML Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Fri Jan 08 16:19:41 2016 +0100
@@ -499,7 +499,7 @@
$ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
|> Syntax.check_term lthy
val def_binding =
- if Config.get lthy function_defs then (Binding.name fdefname, [])
+ if Config.get lthy function_internals then (Binding.name fdefname, [])
else Attrib.empty_binding
in
Local_Theory.define
--- a/src/HOL/Tools/Function/function_lib.ML Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML Fri Jan 08 16:19:41 2016 +0100
@@ -7,7 +7,7 @@
signature FUNCTION_LIB =
sig
- val function_defs: bool Config.T
+ val function_internals: bool Config.T
val plural: string -> string -> 'a list -> string
@@ -32,7 +32,7 @@
structure Function_Lib: FUNCTION_LIB =
struct
-val function_defs = Attrib.setup_config_bool @{binding function_defs} (K false)
+val function_internals = Attrib.setup_config_bool @{binding function_internals} (K false)
(* "The variable" ^ plural " is" "s are" vs *)
--- a/src/HOL/Tools/Function/mutual.ML Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Fri Jan 08 16:19:41 2016 +0100
@@ -129,7 +129,7 @@
fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
let
val def_binding =
- if Config.get lthy function_defs then (Binding.name (Thm.def_name fname), [])
+ if Config.get lthy function_internals then (Binding.name (Thm.def_name fname), [])
else Attrib.empty_binding
val ((f, (_, f_defthm)), lthy') =
Local_Theory.define
--- a/src/HOL/Tools/Function/partial_function.ML Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML Fri Jan 08 16:19:41 2016 +0100
@@ -257,7 +257,8 @@
val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc);
val f_def_binding =
- if Config.get lthy Function_Lib.function_defs then (Binding.name (Thm.def_name fname), [])
+ if Config.get lthy Function_Lib.function_internals
+ then (Binding.name (Thm.def_name fname), [])
else Attrib.empty_binding;
val ((f, (_, f_def)), lthy') = Local_Theory.define
((f_binding, mixfix), (f_def_binding, f_def_rhs)) lthy;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jan 08 16:19:41 2016 +0100
@@ -23,7 +23,7 @@
val fact_of_ref : Proof.context -> Keyword.keywords -> thm list -> status Termtab.table ->
Facts.ref * Token.src list -> ((string * stature) * thm) list
- val backquote_thm : Proof.context -> thm -> string
+ val cartouche_thm : Proof.context -> thm -> string
val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
val clasimpset_rule_table_of : Proof.context -> status Termtab.table
val build_name_tables : (thm -> string) -> ('a * thm) list ->
@@ -81,11 +81,6 @@
| explode_interval max (Facts.From i) = i upto i + max - 1
| explode_interval _ (Facts.Single i) = [i]
-val backquote = enclose "\<open>" "\<close>"
-
-(* unfolding these can yield really huge terms *)
-val risky_defs = @{thms Bit0_def Bit1_def}
-
fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
@@ -168,7 +163,7 @@
fun nth_name j =
(case xref of
- Facts.Fact s => backquote (simplify_spaces (YXML.content_of s)) ^ bracket
+ Facts.Fact s => cartouche (simplify_spaces (YXML.content_of s)) ^ bracket
| Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
| Facts.Named ((name, _), NONE) => make_name keywords (length ths > 1) (j + 1) name ^ bracket
| Facts.Named ((name, _), SOME intervals) =>
@@ -301,8 +296,8 @@
(Term.add_vars t [] |> sort_by (fst o fst))
|> fst
-fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote
-fun backquote_thm ctxt = backquote_term ctxt o Thm.prop_of
+fun cartouche_term ctxt = close_form #> hackish_string_of_term ctxt #> cartouche
+fun cartouche_thm ctxt = cartouche_term ctxt o Thm.prop_of
(* TODO: rewrite to use nets and/or to reuse existing data structures *)
fun clasimpset_rule_table_of ctxt =
@@ -324,7 +319,6 @@
val (rec_defs, nonrec_defs) = specs
|> filter (curry (op =) Spec_Rules.Equational o fst)
|> maps (snd o snd)
- |> filter_out (member Thm.eq_thm_prop risky_defs)
|> List.partition (is_rec_def o Thm.prop_of)
val spec_intros = specs
|> filter (member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] o fst)
@@ -509,7 +503,7 @@
let
fun get_name () =
if name0 = "" orelse name0 = local_thisN then
- backquote_thm ctxt th
+ cartouche_thm ctxt th
else
let val short_name = Facts.extern ctxt facts name0 in
if check_thms short_name then
--- a/src/HOL/Tools/inductive.ML Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Tools/inductive.ML Fri Jan 08 16:19:41 2016 +0100
@@ -71,7 +71,7 @@
signature INDUCTIVE =
sig
include BASIC_INDUCTIVE
- val inductive_defs: bool Config.T
+ val inductive_internals: bool Config.T
val select_disj_tac: Proof.context -> int -> int -> int -> tactic
type add_ind_def =
inductive_flags ->
@@ -122,7 +122,7 @@
(** misc utilities **)
-val inductive_defs = Attrib.setup_config_bool @{binding inductive_defs} (K false);
+val inductive_internals = Attrib.setup_config_bool @{binding inductive_internals} (K false);
fun message quiet_mode s = if quiet_mode then () else writeln s;
@@ -849,16 +849,13 @@
else alt_name;
val rec_name = Binding.name_of rec_binding;
- val inductive_defs = Config.get lthy inductive_defs;
- fun cond_def_binding b =
- if inductive_defs then Binding.reset_pos (Thm.def_binding b)
- else Binding.empty;
+ val internals = Config.get lthy inductive_internals;
val ((rec_const, (_, fp_def)), lthy') = lthy
|> is_auxiliary ? Proof_Context.concealed
|> Local_Theory.define
((rec_binding, case cnames_syn of [(_, mx)] => mx | _ => NoSyn),
- ((cond_def_binding rec_binding, @{attributes [nitpick_unfold]}),
+ ((Thm.make_def_binding internals rec_binding, @{attributes [nitpick_unfold]}),
fold_rev lambda params
(Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
||> Proof_Context.restore_naming lthy;
@@ -874,7 +871,7 @@
map Free (Variable.variant_frees lthy' intr_ts (mk_names "x" (length Ts) ~~ Ts));
in
((b, mx),
- ((cond_def_binding b, []), fold_rev lambda (params @ xs)
+ ((Thm.make_def_binding internals b, []), fold_rev lambda (params @ xs)
(list_comb (rec_const, params @ make_bool_args' bs i @
make_args argTs (xs ~~ Ts)))))
end) (cnames_syn ~~ cs)
@@ -887,7 +884,7 @@
val mono = prove_mono quiet_mode skip_mono predT fp_fun monos ctxt'';
val (_, lthy''') = lthy''
|> Local_Theory.note
- ((if inductive_defs
+ ((if internals
then Binding.qualify true rec_name (Binding.name "mono")
else Binding.empty, []),
Proof_Context.export ctxt'' lthy'' [mono]);
--- a/src/HOL/Transitive_Closure.thy Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/Transitive_Closure.thy Fri Jan 08 16:19:41 2016 +0100
@@ -21,7 +21,7 @@
\<close>
context
- notes [[inductive_defs]]
+ notes [[inductive_internals]]
begin
inductive_set rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" ("(_\<^sup>*)" [1000] 999)
--- a/src/Pure/General/pretty.ML Fri Jan 08 15:27:16 2016 +0100
+++ b/src/Pure/General/pretty.ML Fri Jan 08 16:19:41 2016 +0100
@@ -45,7 +45,6 @@
val paragraph: T list -> T
val para: string -> T
val quote: T -> T
- val backquote: T -> T
val cartouche: T -> T
val separate: string -> T list -> T list
val commas: T list -> T list
@@ -168,7 +167,6 @@
val para = paragraph o text;
fun quote prt = blk (1, [str "\"", prt, str "\""]);
-fun backquote prt = blk (1, [str "`", prt, str "`"]);
fun cartouche prt = blk (1, [str "\\<open>", prt, str "\\<close>"]);
fun separate sep prts =
--- a/src/Pure/Isar/bundle.ML Fri Jan 08 15:27:16 2016 +0100
+++ b/src/Pure/Isar/bundle.ML Fri Jan 08 16:19:41 2016 +0100
@@ -124,7 +124,7 @@
fun print_bundles verbose ctxt =
let
- val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt;
+ val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
fun prt_fact (ths, []) = map prt_thm ths
| prt_fact (ths, atts) = Pretty.enclose "(" ")"
--- a/src/Pure/Isar/element.ML Fri Jan 08 15:27:16 2016 +0100
+++ b/src/Pure/Isar/element.ML Fri Jan 08 16:19:41 2016 +0100
@@ -152,7 +152,7 @@
let
val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
- val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt;
+ val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
fun prt_binding (b, atts) =
Attrib.pretty_binding ctxt (b, if show_attribs then atts else []);
--- a/src/Pure/Isar/token.ML Fri Jan 08 15:27:16 2016 +0100
+++ b/src/Pure/Isar/token.ML Fri Jan 08 16:19:41 2016 +0100
@@ -471,7 +471,7 @@
| SOME (Typ T) => Syntax.pretty_typ ctxt T
| SOME (Term t) => Syntax.pretty_term ctxt t
| SOME (Fact (_, ths)) =>
- Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Thm.pretty_thm ctxt) ths))
+ Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.cartouche o Thm.pretty_thm ctxt) ths))
| _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok));
--- a/src/Pure/more_thm.ML Fri Jan 08 15:27:16 2016 +0100
+++ b/src/Pure/more_thm.ML Fri Jan 08 16:19:41 2016 +0100
@@ -92,6 +92,7 @@
val def_name_optional: string -> string -> string
val def_binding: Binding.binding -> Binding.binding
val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding
+ val make_def_binding: bool -> Binding.binding -> Binding.binding
val has_name_hint: thm -> bool
val get_name_hint: thm -> string
val put_name_hint: string -> thm -> thm
@@ -570,6 +571,9 @@
fun def_binding_optional b name =
if Binding.is_empty name then def_binding b else name;
+fun make_def_binding cond b =
+ if cond then Binding.reset_pos (def_binding b) else Binding.empty;
+
(* unofficial theorem names *)
--- a/src/Tools/jEdit/src/document_view.scala Fri Jan 08 15:27:16 2016 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Fri Jan 08 16:19:41 2016 +0100
@@ -256,7 +256,7 @@
text_area.getGutter.addExtension(gutter_painter)
text_area.addKeyListener(key_listener)
text_area.addCaretListener(caret_listener)
- text_area.addLeftOfScrollBar(overview)
+ text_area.addLeftOfScrollBar(overview); text_area.revalidate(); text_area.repaint()
Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
foreach(text_area.addStructureMatcher(_))
session.raw_edits += main
@@ -271,7 +271,7 @@
session.commands_changed -= main
Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
foreach(text_area.removeStructureMatcher(_))
- text_area.removeLeftOfScrollBar(overview); overview.revoke()
+ overview.revoke(); text_area.removeLeftOfScrollBar(overview)
text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
text_area.removeKeyListener(key_listener)
text_area.getGutter.removeExtension(gutter_painter)
--- a/src/Tools/jEdit/src/text_overview.scala Fri Jan 08 15:27:16 2016 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala Fri Jan 08 16:19:41 2016 +0100
@@ -82,7 +82,13 @@
val rendering = doc_view.get_rendering()
val overview = get_overview()
- if (!rendering.snapshot.is_outdated && overview == current_overview) {
+ if (rendering.snapshot.is_outdated || overview != current_overview) {
+ invoke()
+
+ gfx.setColor(rendering.outdated_color)
+ gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
+ }
+ else {
gfx.setColor(getBackground)
gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
for ((color, h, h1) <- current_colors) {
@@ -90,10 +96,6 @@
gfx.fillRect(0, h, getWidth, h1 - h)
}
}
- else {
- gfx.setColor(rendering.outdated_color)
- gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
- }
}
}
}