--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy Mon Mar 24 15:31:17 2014 +0000
@@ -86,7 +86,6 @@
apply (erule lt.exhaust)
using [[simproc del: alpha_lst]]
apply (simp_all)
- apply blast
apply (simp add: Abs1_eq_iff CPS.eqvt)
by blast
--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Mon Mar 24 15:31:17 2014 +0000
@@ -48,7 +48,6 @@
apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
using [[simproc del: alpha_lst]]
apply (auto simp add: fresh_star_def)
- apply blast+
apply (erule Abs_lst1_fcb)
apply (simp_all add: Abs_fresh_iff)
apply (erule fresh_eqvt_at)
@@ -82,7 +81,6 @@
apply (rule_tac y="a" in lt.exhaust)
using [[simproc del: alpha_lst]]
apply auto
- apply blast
apply (rule_tac x="lt" and ?'a="name" in obtain_fresh)
apply (simp add: Abs1_eq_iff)
apply blast+
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Mon Mar 24 15:31:17 2014 +0000
@@ -26,7 +26,6 @@
apply (case_tac b)
apply (rule_tac y="a" in lt.strong_exhaust)
apply auto[3]
- apply blast+
apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
apply (simp add: fresh_at_base Abs1_eq_iff)
--"-"
--- a/Nominal/Ex/CPS/Lt.thy Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/CPS/Lt.thy Mon Mar 24 15:31:17 2014 +0000
@@ -24,7 +24,6 @@
apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust)
apply blast
apply(simp_all add: fresh_star_def fresh_Pair_elim)
- apply blast
apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
apply(simp add: Abs_fresh_iff)
apply(simp add: fresh_star_def fresh_Pair)
--- a/Nominal/Ex/Lambda.thy Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/Lambda.thy Mon Mar 24 15:31:17 2014 +0000
@@ -661,12 +661,9 @@
apply (case_tac a rule: lam.exhaust)
using [[simproc del: alpha_lst]]
apply simp_all[3]
- apply blast
apply (case_tac b)
apply (rule_tac y="a" and c="ba" in lam.strong_exhaust)
apply simp_all[3]
- apply blast
- apply blast
apply (simp add: Abs1_eq_iff fresh_star_def)
using [[simproc del: alpha_lst]]
apply(simp_all)
@@ -713,8 +710,6 @@
apply (rule_tac y="a" in lam.exhaust)
using [[simproc del: alpha_lst]]
apply simp_all
-apply blast
-apply blast
apply (rule_tac x="(name, lam)" and ?'a="name" in obtain_fresh)
apply blast
apply clarify
--- a/Nominal/Ex/Let.thy Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/Let.thy Mon Mar 24 15:31:17 2014 +0000
@@ -86,7 +86,6 @@
apply(case_tac x)
apply(case_tac b rule: trm_assn.exhaust(2))
apply(simp_all)
-apply(blast)
done
termination by lexicographic_order
@@ -145,7 +144,6 @@
apply(case_tac x)
apply(case_tac b rule: trm_assn.exhaust(2))
apply(simp_all)
- apply(blast)
done
termination by lexicographic_order
--- a/Nominal/Ex/Multi_Recs2.thy Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/Multi_Recs2.thy Mon Mar 24 15:31:17 2014 +0000
@@ -103,7 +103,6 @@
apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *})
apply(rule_tac y="exp" and c="c" in fun_recs.strong_exhaust(1))
apply(simp_all)[4]
- apply(blast)
apply(rule_tac ya="fnclause" and c="c" in fun_recs.strong_exhaust(2))
apply(blast)
apply(rule_tac yb="fnclauses" in fun_recs.strong_exhaust(3))
--- a/Nominal/Ex/Pi.thy Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/Pi.thy Mon Mar 24 15:31:17 2014 +0000
@@ -172,8 +172,6 @@
apply(auto simp add: fresh_star_def)[1]
apply(blast)
apply(simp)
- apply(blast)
- apply(simp)
apply(case_tac b)
apply(simp)
apply(case_tac a)
@@ -192,9 +190,7 @@
apply(blast)
using [[simproc del: alpha_lst]]
apply(auto simp add: fresh_star_def)[1]
- apply(blast)
apply(simp)
- apply(blast)
--"compatibility"
apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")
--- a/Nominal/Nominal2.thy Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Nominal2.thy Mon Mar 24 15:31:17 2014 +0000
@@ -569,7 +569,7 @@
(* FIXME: local version *)
(* val (_, spec_ctxt') = Proof_Context.add_fixes constr_trms spec_ctxt *)
- val thy' = Sign.add_consts_i constr_trms (Proof_Context.theory_of spec_ctxt)
+ val thy' = Sign.add_consts constr_trms (Proof_Context.theory_of spec_ctxt)
in
(dts', thy')
end
@@ -591,7 +591,7 @@
in
(Local_Theory.exit_global lthy')
- |> Sign.add_consts_i bn_funs'
+ |> Sign.add_consts bn_funs'
|> pair (bn_funs', bn_eqs)
end
*}
--- a/Nominal/Nominal2_Base.thy Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Nominal2_Base.thy Mon Mar 24 15:31:17 2014 +0000
@@ -2167,7 +2167,7 @@
proof -
have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_of M})" by simp
also have "... \<subseteq> (\<Union>x \<in> set_of M. supp x)" by auto
- also have "... = supp (set_of M)" by (simp add: subst supp_of_finite_sets)
+ also have "... = supp (set_of M)" by (simp add: supp_of_finite_sets)
also have " ... \<subseteq> supp M" by (rule supp_set_of)
finally show "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" .
qed
--- a/Nominal/nominal_function.ML Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/nominal_function.ML Mon Mar 24 15:31:17 2014 +0000
@@ -205,7 +205,7 @@
end
val add_nominal_function =
- gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
+ gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type})
fun add_nominal_function_cmd a b c d int =
gen_add_nominal_function int Specification.read_spec "_::type" a b c d
@@ -220,7 +220,7 @@
end
val nominal_function =
- gen_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
+ gen_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type})
fun nominal_function_cmd a b c int =
gen_nominal_function int Specification.read_spec "_::type" a b c
--- a/Nominal/nominal_inductive.ML Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/nominal_inductive.ML Mon Mar 24 15:31:17 2014 +0000
@@ -32,8 +32,8 @@
(* fixme: move to nominal_library *)
fun real_head_of (@{term Trueprop} $ t) = real_head_of t
- | real_head_of (Const ("==>", _) $ _ $ t) = real_head_of t
- | real_head_of (Const (@{const_name all}, _) $ Abs (_, _, t)) = real_head_of t
+ | real_head_of (Const (@{const_name Pure.imp}, _) $ _ $ t) = real_head_of t
+ | real_head_of (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = real_head_of t
| real_head_of (Const (@{const_name All}, _) $ Abs (_, _, t)) = real_head_of t
| real_head_of (Const ("HOL.induct_forall", _) $ Abs (_, _, t)) = real_head_of t
| real_head_of t = head_of t
--- a/Nominal/nominal_library.ML Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/nominal_library.ML Mon Mar 24 15:31:17 2014 +0000
@@ -298,7 +298,8 @@
(* decompses a formula into params, premises and a conclusion *)
fun strip_full_horn trm =
let
- fun strip_outer_params (Const ("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T)
+ fun strip_outer_params (Const (@{const_name Pure.all}, _) $ Abs (a, T, t)) =
+ strip_outer_params t |>> cons (a, T)
| strip_outer_params B = ([], B)
val (params, body) = strip_outer_params trm
--- a/Nominal/nominal_mutual.ML Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/nominal_mutual.ML Mon Mar 24 15:31:17 2014 +0000
@@ -291,7 +291,7 @@
end
-fun forall_elim s (Const ("all", _) $ Abs (_, _, t)) = subst_bound (s, t)
+fun forall_elim s (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = subst_bound (s, t)
| forall_elim _ t = t
val forall_elim_list = fold forall_elim
@@ -316,7 +316,7 @@
val acc_prems =
map prop_of induct_thms
|> map2 forall_elim_list argss
- |> map (strip_qnt_body "all")
+ |> map (strip_qnt_body @{const_name Pure.all})
|> map (curry Logic.nth_prem 1)
|> map HOLogic.dest_Trueprop
--- a/Nominal/nominal_thmdecls.ML Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/nominal_thmdecls.ML Mon Mar 24 15:31:17 2014 +0000
@@ -112,7 +112,7 @@
Syntax.string_of_term (Context.proof_of context) (prop_of thm))
in
case prop_of thm of
- Const ("==", _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' =>
+ Const ("Pure.eq", _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' =>
if is_Var p andalso is_fixed (Context.proof_of context) c andalso c aconv c' then
c
else
@@ -256,7 +256,7 @@
fun eqvt_transform ctxt thm =
(case prop_of thm of @{const "Trueprop"} $ _ =>
thm_4_of_1 ctxt thm
- | @{const "==>"} $ _ $ _ =>
+ | @{const "Pure.imp"} $ _ $ _ =>
thm_4_of_1 ctxt (thm_1_of_2 ctxt thm)
| _ =>
error msg)
@@ -279,7 +279,7 @@
in
(th', thm_4_of_1 ctxt thm)
end
- | @{const "==>"} $ _ $ _ =>
+ | @{const "Pure.imp"} $ _ $ _ =>
let
val th1 = thm_1_of_2 ctxt thm
in