--- a/src/HOL/Nominal/Examples/Crary.thy Wed Sep 05 19:58:09 2012 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy Wed Sep 05 20:36:13 2012 +0200
@@ -225,7 +225,7 @@
assumes a: "x\<sharp>\<theta>"
shows "\<theta><Var x> = Var x"
using a
-by (induct \<theta> arbitrary: x, auto simp add:fresh_list_cons fresh_prod fresh_atm)
+by (induct \<theta> arbitrary: x) (auto simp add:fresh_list_cons fresh_prod fresh_atm)
lemma psubst_subst_propagate:
assumes "x\<sharp>\<theta>"
@@ -529,7 +529,7 @@
lemma alg_path_equiv_implies_valid:
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>"
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>"
-by (induct rule : alg_equiv_alg_path_equiv.inducts, auto)
+by (induct rule : alg_equiv_alg_path_equiv.inducts) auto
lemma algorithmic_symmetry:
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<Leftrightarrow> s : T"
--- a/src/HOL/Nominal/Examples/Fsub.thy Wed Sep 05 19:58:09 2012 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy Wed Sep 05 20:36:13 2012 +0200
@@ -140,12 +140,12 @@
lemma finite_vrs:
shows "finite (tyvrs_of x)"
and "finite (vrs_of x)"
-by (nominal_induct rule:binding.strong_induct, auto)
+by (nominal_induct rule:binding.strong_induct) auto
lemma finite_doms:
shows "finite (ty_dom \<Gamma>)"
and "finite (trm_dom \<Gamma>)"
-by (induct \<Gamma>, auto simp add: finite_vrs)
+by (induct \<Gamma>) (auto simp add: finite_vrs)
lemma ty_dom_supp:
shows "(supp (ty_dom \<Gamma>)) = (ty_dom \<Gamma>)"
@@ -155,13 +155,13 @@
lemma ty_dom_inclusion:
assumes a: "(TVarB X T)\<in>set \<Gamma>"
shows "X\<in>(ty_dom \<Gamma>)"
-using a by (induct \<Gamma>, auto)
+using a by (induct \<Gamma>) (auto)
lemma ty_binding_existence:
assumes "X \<in> (tyvrs_of a)"
shows "\<exists>T.(TVarB X T=a)"
using assms
-by (nominal_induct a rule: binding.strong_induct, auto)
+by (nominal_induct a rule: binding.strong_induct) (auto)
lemma ty_dom_existence:
assumes a: "X\<in>(ty_dom \<Gamma>)"
@@ -176,7 +176,7 @@
lemma doms_append:
shows "ty_dom (\<Gamma>@\<Delta>) = ((ty_dom \<Gamma>) \<union> (ty_dom \<Delta>))"
and "trm_dom (\<Gamma>@\<Delta>) = ((trm_dom \<Gamma>) \<union> (trm_dom \<Delta>))"
- by (induct \<Gamma>, auto)
+ by (induct \<Gamma>) (auto)
lemma ty_vrs_prm_simp:
fixes pi::"vrs prm"
@@ -1069,7 +1069,7 @@
lemma typing_ok:
assumes "\<Gamma> \<turnstile> t : T"
shows "\<turnstile> \<Gamma> ok"
-using assms by (induct, auto)
+using assms by (induct) (auto)
nominal_inductive typing
by (auto dest!: typing_ok intro: closed_in_fresh fresh_dom type_subst_fresh
@@ -1208,7 +1208,7 @@
lemma ty_dom_cons:
shows "ty_dom (\<Gamma>@[VarB X Q]@\<Delta>) = ty_dom (\<Gamma>@\<Delta>)"
-by (induct \<Gamma>, auto)
+by (induct \<Gamma>) (auto)
lemma closed_in_cons:
assumes "S closed_in (\<Gamma> @ VarB X Q # \<Delta>)"
@@ -1251,7 +1251,7 @@
lemma ty_dom_vrs:
shows "ty_dom (G @ [VarB x Q] @ D) = ty_dom (G @ D)"
-by (induct G, auto)
+by (induct G) (auto)
lemma valid_cons':
assumes "\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok"
--- a/src/HOL/Nominal/Examples/SOS.thy Wed Sep 05 19:58:09 2012 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy Wed Sep 05 20:36:13 2012 +0200
@@ -321,7 +321,7 @@
proof (nominal_induct e e\<^isub>1 avoiding: e\<^isub>2 rule: big.strong_induct)
case (b_Lam x e t\<^isub>2)
have "Lam [x].e \<Down> t\<^isub>2" by fact
- thus "Lam [x].e = t\<^isub>2" by (cases, simp_all add: trm.inject)
+ thus "Lam [x].e = t\<^isub>2" by cases (simp_all add: trm.inject)
next
case (b_App x e\<^isub>1 e\<^isub>2 e' e\<^isub>1' e\<^isub>2' t\<^isub>2)
have ih1: "\<And>t. e\<^isub>1 \<Down> t \<Longrightarrow> Lam [x].e\<^isub>1' = t" by fact
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Sep 05 19:58:09 2012 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Sep 05 20:36:13 2012 +0200
@@ -527,7 +527,7 @@
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global
{quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
- coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
+ coind = false, no_elim = true, no_ind = false, skip_mono = true}
(map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
(rep_set_names' ~~ recTs'))
[] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
@@ -1484,7 +1484,7 @@
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global
{quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
- coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
+ coind = false, no_elim = false, no_ind = false, skip_mono = true}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
(map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
--- a/src/HOL/Tools/Datatype/datatype.ML Wed Sep 05 19:58:09 2012 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Wed Sep 05 20:36:13 2012 +0200
@@ -178,7 +178,7 @@
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global
{quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
- coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
+ coind = false, no_elim = true, no_ind = false, skip_mono = true}
(map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
(map (fn x => (Attrib.empty_binding, x)) intr_ts) []
||> Sign.restore_naming thy1
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Wed Sep 05 19:58:09 2012 +0200
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Wed Sep 05 20:36:13 2012 +0200
@@ -145,7 +145,7 @@
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global
{quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
- coind = false, no_elim = false, no_ind = true, skip_mono = true, fork_mono = false}
+ coind = false, no_elim = false, no_ind = true, skip_mono = true}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
(map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
--- a/src/HOL/Tools/Function/function_core.ML Wed Sep 05 19:58:09 2012 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Wed Sep 05 20:36:13 2012 +0200
@@ -439,8 +439,7 @@
coind = false,
no_elim = false,
no_ind = false,
- skip_mono = true,
- fork_mono = false}
+ skip_mono = true}
[binding] (* relation *)
[] (* no parameters *)
(map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
--- a/src/HOL/Tools/inductive.ML Wed Sep 05 19:58:09 2012 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Sep 05 20:36:13 2012 +0200
@@ -39,7 +39,7 @@
thm list list * local_theory
type inductive_flags =
{quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
- no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
+ no_elim: bool, no_ind: bool, skip_mono: bool}
val add_inductive_i:
inductive_flags -> ((binding * typ) * mixfix) list ->
(string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
@@ -358,10 +358,10 @@
(* prove monotonicity *)
-fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
- (message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
+fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt =
+ (message (quiet_mode orelse skip_mono andalso ! quick_and_dirty)
" Proving monotonicity ...";
- (if skip_mono then Skip_Proof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
+ (if skip_mono then Skip_Proof.prove else Goal.prove_future) ctxt
[] []
(HOLogic.mk_Trueprop
(Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
@@ -746,8 +746,7 @@
(** specification of (co)inductive predicates **)
-fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind
- cs intr_ts monos params cnames_syn lthy =
+fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn lthy =
let
val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
@@ -841,7 +840,7 @@
val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
- val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy''';
+ val mono = prove_mono quiet_mode skip_mono predT fp_fun monos lthy''';
val (_, lthy'''') =
Local_Theory.note (apfst Binding.conceal Attrib.empty_binding,
Proof_Context.export lthy''' lthy'' [mono]) lthy'';
@@ -912,7 +911,7 @@
type inductive_flags =
{quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
- no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool};
+ no_elim: bool, no_ind: bool, skip_mono: bool};
type add_ind_def =
inductive_flags ->
@@ -920,7 +919,7 @@
term list -> (binding * mixfix) list ->
local_theory -> inductive_result * local_theory;
-fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
+fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono}
cs intros monos params cnames_syn lthy =
let
val _ = null cnames_syn andalso error "No inductive predicates given";
@@ -933,7 +932,7 @@
apfst split_list (split_list (map (check_rule lthy cs params) intros));
val (lthy1, lthy2, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
- argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts
+ argTs, bs, xs) = mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts
monos params cnames_syn lthy;
val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
@@ -983,7 +982,7 @@
(* external interfaces *)
fun gen_add_inductive_i mk_def
- (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
+ (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono})
cnames_syn pnames spec monos lthy =
let
val thy = Proof_Context.theory_of lthy;
@@ -1047,8 +1046,9 @@
|> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
val (cs, ps) = chop (length cnames_syn) vars;
val monos = Attrib.eval_thms lthy raw_monos;
- val flags = {quiet_mode = false, verbose = verbose, alt_name = Binding.empty,
- coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int};
+ val flags =
+ {quiet_mode = false, verbose = verbose, alt_name = Binding.empty,
+ coind = coind, no_elim = false, no_ind = false, skip_mono = false};
in
lthy
|> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos
--- a/src/HOL/Tools/inductive_realizer.ML Wed Sep 05 19:58:09 2012 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Sep 05 20:36:13 2012 +0200
@@ -355,7 +355,7 @@
val (ind_info, thy3') = thy2 |>
Inductive.add_inductive_global
{quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
- no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
+ no_elim = false, no_ind = false, skip_mono = false}
rlzpreds rlzparams (map (fn (rintr, intr) =>
((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
subst_atomic rlzpreds' (Logic.unvarify_global rintr)))
--- a/src/HOL/Tools/inductive_set.ML Wed Sep 05 19:58:09 2012 +0200
+++ b/src/HOL/Tools/inductive_set.ML Wed Sep 05 20:36:13 2012 +0200
@@ -417,7 +417,7 @@
(**** definition of inductive sets ****)
fun add_ind_set_def
- {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
+ {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono}
cs intros monos params cnames_syn lthy =
let
val thy = Proof_Context.theory_of lthy;
@@ -490,8 +490,7 @@
val ({preds, intrs, elims, raw_induct, eqs, ...}, lthy1) =
Inductive.add_ind_def
{quiet_mode = quiet_mode, verbose = verbose, alt_name = Binding.empty,
- coind = coind, no_elim = no_elim, no_ind = no_ind,
- skip_mono = skip_mono, fork_mono = fork_mono}
+ coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
cs' intros' monos' params1 cnames_syn' lthy;
(* define inductive sets using previously defined predicates *)
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Wed Sep 05 19:58:09 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Wed Sep 05 20:36:13 2012 +0200
@@ -92,9 +92,9 @@
private val subexp_include =
Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
- Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND,
- Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE,
- Isabelle_Markup.DOC_SOURCE)
+ Isabelle_Markup.PATH, Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM,
+ Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR,
+ Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOC_SOURCE)
def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Color]] =
{
@@ -190,8 +190,8 @@
Isabelle_Markup.DOC_SOURCE -> "document source")
private val tooltip_elements =
- Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING) ++
- tooltips.keys
+ Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING,
+ Isabelle_Markup.PATH) ++ tooltips.keys
private def string_of_typing(kind: String, body: XML.Body): String =
Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
@@ -208,6 +208,10 @@
{
case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) =>
add(prev, r, (true, kind + " " + quote(name)))
+ case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Path(name), _)))
+ if Path.is_ok(name) =>
+ val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
+ add(prev, r, (true, "file " + quote(jedit_file)))
case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body))) =>
add(prev, r, (true, string_of_typing("::", body)))
case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) =>