--- a/doc-src/Locales/Locales/Locales.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/doc-src/Locales/Locales/Locales.thy Sat Mar 29 19:14:00 2008 +0100
@@ -398,7 +398,7 @@
predicate is defined.
*}
(*<*)
-ML_setup {*
+ML {*
val [comm_semi_ax1, comm_semi_ax2] = thms "comm_semi.axioms";
bind_thm ("comm_semi_ax1", comm_semi_ax1);
bind_thm ("comm_semi_ax2", comm_semi_ax2);
--- a/src/CCL/Term.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/CCL/Term.thy Sat Mar 29 19:14:00 2008 +0100
@@ -220,7 +220,7 @@
end
*}
-ML_setup {*
+ML {*
bind_thm ("ifBtrue", mk_beta_rl "if true then t else u = t");
bind_thm ("ifBfalse", mk_beta_rl "if false then t else u = u");
bind_thm ("ifBbot", mk_beta_rl "if bot then t else u = bot");
@@ -272,7 +272,7 @@
subsection {* Constructors are injective *}
-ML_setup {*
+ML {*
bind_thms ("term_injs", map (mk_inj_rl (the_context ())
[thm "applyB", thm "splitB", thm "whenBinl", thm "whenBinr", thm "ncaseBsucc", thm "lcaseBcons"])
@@ -285,7 +285,7 @@
subsection {* Constructors are distinct *}
-ML_setup {*
+ML {*
bind_thms ("term_dstncts",
mkall_dstnct_thms (the_context ()) (thms "data_defs") (thms "ccl_injs" @ thms "term_injs")
[["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
@@ -294,7 +294,7 @@
subsection {* Rules for pre-order @{text "[="} *}
-ML_setup {*
+ML {*
local
fun mk_thm s = prove_goalw (the_context ()) (thms "data_defs") s (fn _ =>
@@ -311,7 +311,7 @@
subsection {* Rewriting and Proving *}
-ML_setup {*
+ML {*
bind_thms ("term_injDs", XH_to_Ds @{thms term_injs});
*}
--- a/src/FOLP/IFOLP.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/FOLP/IFOLP.thy Sat Mar 29 19:14:00 2008 +0100
@@ -502,7 +502,7 @@
(*special cases for free variables P, Q, R, S -- up to 3 arguments*)
-ML_setup {*
+ML {*
bind_thms ("pred_congs",
flat (map (fn c =>
map (fn th => read_instantiate [("P",c)] th)
--- a/src/HOL/Algebra/abstract/Ring2.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy Sat Mar 29 19:14:00 2008 +0100
@@ -306,7 +306,7 @@
end;
*}
-ML_setup {* Addsimprocs [ring_simproc] *}
+ML {* Addsimprocs [ring_simproc] *}
lemma natsum_ldistr:
"!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Sat Mar 29 19:14:00 2008 +0100
@@ -282,7 +282,7 @@
finally show ?thesis .
qed
-(* ML_setup {* Addsimprocs [ring_simproc] *} *)
+(* ML {* Addsimprocs [ring_simproc] *} *)
instance up :: (ring) ring
proof
@@ -378,7 +378,7 @@
qed
qed
*)
-ML_setup {* Delsimprocs [ring_simproc] *}
+ML {* Delsimprocs [ring_simproc] *}
lemma monom_mult_is_smult:
"monom (a::'a::ring) 0 * p = a *s p"
@@ -393,7 +393,7 @@
then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring
qed
-ML_setup {* Addsimprocs [ring_simproc] *}
+ML {* Addsimprocs [ring_simproc] *}
lemma monom_add [simp]:
"monom (a + b) n = monom (a::'a::ring) n + monom b n"
@@ -442,14 +442,14 @@
(* Polynomials form an algebra *)
-ML_setup {* Delsimprocs [ring_simproc] *}
+ML {* Delsimprocs [ring_simproc] *}
lemma smult_assoc2:
"(a *s p) * q = (a::'a::ring) *s (p * q)"
by (rule up_eqI) (simp add: natsum_rdistr m_assoc)
(* Simproc fails. *)
-ML_setup {* Addsimprocs [ring_simproc] *}
+ML {* Addsimprocs [ring_simproc] *}
(* the following can be derived from the above ones,
for generality reasons, it is therefore done *)
--- a/src/HOL/Bali/AxSem.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Bali/AxSem.thy Sat Mar 29 19:14:00 2008 +0100
@@ -1013,7 +1013,7 @@
apply (auto simp add: type_ok_def)
done
-ML_setup {* bind_thms ("ax_Abrupts", sum3_instantiate @{thm ax_derivs.Abrupt}) *}
+ML {* bind_thms ("ax_Abrupts", sum3_instantiate @{thm ax_derivs.Abrupt}) *}
declare ax_Abrupts [intro!]
lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]
--- a/src/HOL/Bali/Eval.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Bali/Eval.thy Sat Mar 29 19:14:00 2008 +0100
@@ -749,7 +749,7 @@
29(AVar),24(Call)]
*)
-ML_setup {*
+ML {*
bind_thm ("eval_induct_", rearrange_prems
[0,1,2,8,4,30,31,27,15,16,
17,18,19,20,21,3,5,25,26,23,6,
@@ -890,7 +890,7 @@
(_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
| _ => SOME (mk_meta_eq @{thm eval_stmt_eq})) *}
-ML_setup {*
+ML {*
bind_thms ("AbruptIs", sum3_instantiate @{thm eval.Abrupt})
*}
--- a/src/HOL/Bali/Evaln.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Bali/Evaln.thy Sat Mar 29 19:14:00 2008 +0100
@@ -294,7 +294,7 @@
(_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
| _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *}
-ML_setup {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{thm evaln.Abrupt}) *}
+ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{thm evaln.Abrupt}) *}
declare evaln_AbruptIs [intro!]
lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
--- a/src/HOL/Bali/Example.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Bali/Example.thy Sat Mar 29 19:14:00 2008 +0100
@@ -894,7 +894,7 @@
declare member_is_static_simp [simp]
declare wt.Skip [rule del] wt.Init [rule del]
-ML_setup {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
+ML {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
@@ -1192,7 +1192,7 @@
declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
Base_foo_defs [simp]
-ML_setup {* bind_thms ("eval_intros", map
+ML {* bind_thms ("eval_intros", map
(simplify (@{simpset} delsimps @{thms Skip_eq}
addsimps @{thms lvar_def}) o
rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
--- a/src/HOL/Bali/Term.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Bali/Term.thy Sat Mar 29 19:14:00 2008 +0100
@@ -266,7 +266,7 @@
is_stmt :: "term \<Rightarrow> bool"
"is_stmt t \<equiv> \<exists>c. t=In1r c"
-ML_setup {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *}
+ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *}
declare is_stmt_rews [simp]
--- a/src/HOL/IntDiv.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/IntDiv.thy Sat Mar 29 19:14:00 2008 +0100
@@ -257,7 +257,7 @@
text {* Tool setup *}
-ML_setup {*
+ML {*
local
structure CancelDivMod = CancelDivModFun(
--- a/src/HOL/List.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/List.thy Sat Mar 29 19:14:00 2008 +0100
@@ -591,7 +591,7 @@
- or both lists end in the same list.
*}
-ML_setup {*
+ML {*
local
fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
--- a/src/HOL/OrderedGroup.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/OrderedGroup.thy Sat Mar 29 19:14:00 2008 +0100
@@ -1421,7 +1421,7 @@
end);
*}
-ML_setup {*
+ML {*
Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
*}
--- a/src/HOL/Product_Type.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Product_Type.thy Sat Mar 29 19:14:00 2008 +0100
@@ -57,7 +57,7 @@
this rule directly --- it loops!
*}
-ML_setup {*
+ML {*
val unit_eq_proc =
let val unit_meta_eq = mk_meta_eq @{thm unit_eq} in
Simplifier.simproc @{theory} "unit_eq" ["x::unit"]
@@ -323,7 +323,7 @@
lemmas split_tupled_all = split_paired_all unit_all_eq2
-ML_setup {*
+ML {*
(* replace parameters of product type by individual component parameters *)
val safe_full_simp_tac = generic_simp_tac true (true, false, false);
local (* filtering with exists_paired_all is an essential optimization *)
@@ -429,7 +429,7 @@
split_beta}.
*}
-ML_setup {*
+ML {*
local
val cond_split_eta_ss = HOL_basic_ss addsimps [thm "cond_split_eta"]
--- a/src/HOL/Set.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Set.thy Sat Mar 29 19:14:00 2008 +0100
@@ -473,7 +473,7 @@
lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"
by blast
-ML_setup {*
+ML {*
local
val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
--- a/src/HOL/ex/Lagrange.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/ex/Lagrange.thy Sat Mar 29 19:14:00 2008 +0100
@@ -25,7 +25,7 @@
(* These two simprocs are even less efficient than ordered rewriting
and kill the second example: *)
-ML_setup {*
+ML {*
Delsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
*}
--- a/src/HOLCF/Pcpo.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOLCF/Pcpo.thy Sat Mar 29 19:14:00 2008 +0100
@@ -197,7 +197,7 @@
lemma UU_reorient: "(\<bottom> = x) = (x = \<bottom>)"
by auto
-ML_setup {*
+ML {*
local
val meta_UU_reorient = thm "UU_reorient" RS eq_reflection;
fun reorient_proc sg _ (_ $ t $ u) =
--- a/src/Sequents/Washing.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/Sequents/Washing.thy Sat Mar 29 19:14:00 2008 +0100
@@ -35,10 +35,10 @@
(* "activate" definitions for use in proof *)
-ML_setup {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *}
-ML_setup {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *}
-ML_setup {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *}
-ML_setup {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *}
+ML {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *}
+ML {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *}
+ML {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *}
+ML {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *}
(* a load of dirty clothes and two dollars gives you clean clothes *)
--- a/src/ZF/Datatype_ZF.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/ZF/Datatype_ZF.thy Sat Mar 29 19:14:00 2008 +0100
@@ -12,7 +12,7 @@
uses "Tools/datatype_package.ML"
begin
-ML_setup {*
+ML {*
(*Typechecking rules for most datatypes involving univ*)
structure Data_Arg =
struct
--- a/src/ZF/Inductive_ZF.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/ZF/Inductive_ZF.thy Sat Mar 29 19:14:00 2008 +0100
@@ -41,7 +41,7 @@
setup IndCases.setup
setup DatatypeTactics.setup
-ML_setup {*
+ML {*
structure Lfp =
struct
val oper = @{const lfp}
--- a/src/ZF/OrdQuant.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/ZF/OrdQuant.thy Sat Mar 29 19:14:00 2008 +0100
@@ -369,7 +369,7 @@
text {* Setting up the one-point-rule simproc *}
-ML_setup {*
+ML {*
local
val unfold_rex_tac = unfold_tac [@{thm rex_def}];