replaced 'ML_setup' by 'ML';
authorwenzelm
Sat Mar 29 19:14:00 2008 +0100 (2008-03-29)
changeset 26480544cef16045b
parent 26479 3a2efce3e992
child 26481 92e901171cc8
replaced 'ML_setup' by 'ML';
doc-src/Locales/Locales/Locales.thy
src/CCL/Term.thy
src/FOLP/IFOLP.thy
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/Bali/AxSem.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/Term.thy
src/HOL/IntDiv.thy
src/HOL/List.thy
src/HOL/OrderedGroup.thy
src/HOL/Product_Type.thy
src/HOL/Set.thy
src/HOL/ex/Lagrange.thy
src/HOLCF/Pcpo.thy
src/Sequents/Washing.thy
src/ZF/Datatype_ZF.thy
src/ZF/Inductive_ZF.thy
src/ZF/OrdQuant.thy
     1.1 --- a/doc-src/Locales/Locales/Locales.thy	Sat Mar 29 19:13:58 2008 +0100
     1.2 +++ b/doc-src/Locales/Locales/Locales.thy	Sat Mar 29 19:14:00 2008 +0100
     1.3 @@ -398,7 +398,7 @@
     1.4    predicate is defined.
     1.5  *}
     1.6  (*<*)
     1.7 -ML_setup {*
     1.8 +ML {*
     1.9    val [comm_semi_ax1, comm_semi_ax2] = thms "comm_semi.axioms";
    1.10    bind_thm ("comm_semi_ax1", comm_semi_ax1);
    1.11    bind_thm ("comm_semi_ax2", comm_semi_ax2);
     2.1 --- a/src/CCL/Term.thy	Sat Mar 29 19:13:58 2008 +0100
     2.2 +++ b/src/CCL/Term.thy	Sat Mar 29 19:14:00 2008 +0100
     2.3 @@ -220,7 +220,7 @@
     2.4  end
     2.5  *}
     2.6  
     2.7 -ML_setup {*
     2.8 +ML {*
     2.9  bind_thm ("ifBtrue", mk_beta_rl "if true then t else u = t");
    2.10  bind_thm ("ifBfalse", mk_beta_rl "if false then t else u = u");
    2.11  bind_thm ("ifBbot", mk_beta_rl "if bot then t else u = bot");
    2.12 @@ -272,7 +272,7 @@
    2.13  
    2.14  subsection {* Constructors are injective *}
    2.15  
    2.16 -ML_setup {*
    2.17 +ML {*
    2.18  
    2.19  bind_thms ("term_injs", map (mk_inj_rl (the_context ())
    2.20    [thm "applyB", thm "splitB", thm "whenBinl", thm "whenBinr", thm "ncaseBsucc", thm "lcaseBcons"])
    2.21 @@ -285,7 +285,7 @@
    2.22  
    2.23  subsection {* Constructors are distinct *}
    2.24  
    2.25 -ML_setup {*
    2.26 +ML {*
    2.27  bind_thms ("term_dstncts",
    2.28    mkall_dstnct_thms (the_context ()) (thms "data_defs") (thms "ccl_injs" @ thms "term_injs")
    2.29      [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
    2.30 @@ -294,7 +294,7 @@
    2.31  
    2.32  subsection {* Rules for pre-order @{text "[="} *}
    2.33  
    2.34 -ML_setup {*
    2.35 +ML {*
    2.36  
    2.37  local
    2.38    fun mk_thm s = prove_goalw (the_context ()) (thms "data_defs") s (fn _ =>
    2.39 @@ -311,7 +311,7 @@
    2.40  
    2.41  subsection {* Rewriting and Proving *}
    2.42  
    2.43 -ML_setup {*
    2.44 +ML {*
    2.45    bind_thms ("term_injDs", XH_to_Ds @{thms term_injs});
    2.46  *}
    2.47  
     3.1 --- a/src/FOLP/IFOLP.thy	Sat Mar 29 19:13:58 2008 +0100
     3.2 +++ b/src/FOLP/IFOLP.thy	Sat Mar 29 19:14:00 2008 +0100
     3.3 @@ -502,7 +502,7 @@
     3.4  
     3.5  (*special cases for free variables P, Q, R, S -- up to 3 arguments*)
     3.6  
     3.7 -ML_setup {*
     3.8 +ML {*
     3.9    bind_thms ("pred_congs",
    3.10      flat (map (fn c =>
    3.11                 map (fn th => read_instantiate [("P",c)] th)
     4.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Sat Mar 29 19:13:58 2008 +0100
     4.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Sat Mar 29 19:14:00 2008 +0100
     4.3 @@ -306,7 +306,7 @@
     4.4    end;
     4.5  *}
     4.6  
     4.7 -ML_setup {* Addsimprocs [ring_simproc] *}
     4.8 +ML {* Addsimprocs [ring_simproc] *}
     4.9  
    4.10  lemma natsum_ldistr:
    4.11    "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
     5.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Sat Mar 29 19:13:58 2008 +0100
     5.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Sat Mar 29 19:14:00 2008 +0100
     5.3 @@ -282,7 +282,7 @@
     5.4    finally show ?thesis .
     5.5  qed
     5.6  
     5.7 -(* ML_setup {* Addsimprocs [ring_simproc] *} *)
     5.8 +(* ML {* Addsimprocs [ring_simproc] *} *)
     5.9  
    5.10  instance up :: (ring) ring
    5.11  proof
    5.12 @@ -378,7 +378,7 @@
    5.13    qed
    5.14  qed
    5.15  *)
    5.16 -ML_setup {* Delsimprocs [ring_simproc] *}
    5.17 +ML {* Delsimprocs [ring_simproc] *}
    5.18  
    5.19  lemma monom_mult_is_smult:
    5.20    "monom (a::'a::ring) 0 * p = a *s p"
    5.21 @@ -393,7 +393,7 @@
    5.22    then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring
    5.23  qed
    5.24  
    5.25 -ML_setup {* Addsimprocs [ring_simproc] *}
    5.26 +ML {* Addsimprocs [ring_simproc] *}
    5.27  
    5.28  lemma monom_add [simp]:
    5.29    "monom (a + b) n = monom (a::'a::ring) n + monom b n"
    5.30 @@ -442,14 +442,14 @@
    5.31  
    5.32  (* Polynomials form an algebra *)
    5.33  
    5.34 -ML_setup {* Delsimprocs [ring_simproc] *}
    5.35 +ML {* Delsimprocs [ring_simproc] *}
    5.36  
    5.37  lemma smult_assoc2:
    5.38    "(a *s p) * q = (a::'a::ring) *s (p * q)"
    5.39  by (rule up_eqI) (simp add: natsum_rdistr m_assoc)
    5.40  (* Simproc fails. *)
    5.41  
    5.42 -ML_setup {* Addsimprocs [ring_simproc] *}
    5.43 +ML {* Addsimprocs [ring_simproc] *}
    5.44  
    5.45  (* the following can be derived from the above ones,
    5.46     for generality reasons, it is therefore done *)
     6.1 --- a/src/HOL/Bali/AxSem.thy	Sat Mar 29 19:13:58 2008 +0100
     6.2 +++ b/src/HOL/Bali/AxSem.thy	Sat Mar 29 19:14:00 2008 +0100
     6.3 @@ -1013,7 +1013,7 @@
     6.4  apply  (auto simp add: type_ok_def)
     6.5  done
     6.6  
     6.7 -ML_setup {* bind_thms ("ax_Abrupts", sum3_instantiate @{thm ax_derivs.Abrupt}) *}
     6.8 +ML {* bind_thms ("ax_Abrupts", sum3_instantiate @{thm ax_derivs.Abrupt}) *}
     6.9  declare ax_Abrupts [intro!]
    6.10  
    6.11  lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]
     7.1 --- a/src/HOL/Bali/Eval.thy	Sat Mar 29 19:13:58 2008 +0100
     7.2 +++ b/src/HOL/Bali/Eval.thy	Sat Mar 29 19:14:00 2008 +0100
     7.3 @@ -749,7 +749,7 @@
     7.4   29(AVar),24(Call)]
     7.5  *)
     7.6  
     7.7 -ML_setup {*
     7.8 +ML {*
     7.9  bind_thm ("eval_induct_", rearrange_prems 
    7.10  [0,1,2,8,4,30,31,27,15,16,
    7.11   17,18,19,20,21,3,5,25,26,23,6,
    7.12 @@ -890,7 +890,7 @@
    7.13        (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
    7.14      | _ => SOME (mk_meta_eq @{thm eval_stmt_eq})) *}
    7.15  
    7.16 -ML_setup {*
    7.17 +ML {*
    7.18  bind_thms ("AbruptIs", sum3_instantiate @{thm eval.Abrupt})
    7.19  *}
    7.20  
     8.1 --- a/src/HOL/Bali/Evaln.thy	Sat Mar 29 19:13:58 2008 +0100
     8.2 +++ b/src/HOL/Bali/Evaln.thy	Sat Mar 29 19:14:00 2008 +0100
     8.3 @@ -294,7 +294,7 @@
     8.4        (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
     8.5      | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *}
     8.6  
     8.7 -ML_setup {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{thm evaln.Abrupt}) *}
     8.8 +ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{thm evaln.Abrupt}) *}
     8.9  declare evaln_AbruptIs [intro!]
    8.10  
    8.11  lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
     9.1 --- a/src/HOL/Bali/Example.thy	Sat Mar 29 19:13:58 2008 +0100
     9.2 +++ b/src/HOL/Bali/Example.thy	Sat Mar 29 19:14:00 2008 +0100
     9.3 @@ -894,7 +894,7 @@
     9.4  
     9.5  declare member_is_static_simp [simp]
     9.6  declare wt.Skip [rule del] wt.Init [rule del]
     9.7 -ML_setup {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
     9.8 +ML {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
     9.9  lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
    9.10  lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
    9.11  
    9.12 @@ -1192,7 +1192,7 @@
    9.13  declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
    9.14          Base_foo_defs  [simp]
    9.15  
    9.16 -ML_setup {* bind_thms ("eval_intros", map 
    9.17 +ML {* bind_thms ("eval_intros", map 
    9.18          (simplify (@{simpset} delsimps @{thms Skip_eq}
    9.19                               addsimps @{thms lvar_def}) o 
    9.20           rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
    10.1 --- a/src/HOL/Bali/Term.thy	Sat Mar 29 19:13:58 2008 +0100
    10.2 +++ b/src/HOL/Bali/Term.thy	Sat Mar 29 19:14:00 2008 +0100
    10.3 @@ -266,7 +266,7 @@
    10.4    is_stmt :: "term \<Rightarrow> bool"
    10.5   "is_stmt t \<equiv> \<exists>c. t=In1r c"
    10.6  
    10.7 -ML_setup {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *}
    10.8 +ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *}
    10.9  
   10.10  declare is_stmt_rews [simp]
   10.11  
    11.1 --- a/src/HOL/IntDiv.thy	Sat Mar 29 19:13:58 2008 +0100
    11.2 +++ b/src/HOL/IntDiv.thy	Sat Mar 29 19:14:00 2008 +0100
    11.3 @@ -257,7 +257,7 @@
    11.4  
    11.5  text {* Tool setup *}
    11.6  
    11.7 -ML_setup {*
    11.8 +ML {*
    11.9  local 
   11.10  
   11.11  structure CancelDivMod = CancelDivModFun(
    12.1 --- a/src/HOL/List.thy	Sat Mar 29 19:13:58 2008 +0100
    12.2 +++ b/src/HOL/List.thy	Sat Mar 29 19:14:00 2008 +0100
    12.3 @@ -591,7 +591,7 @@
    12.4  - or both lists end in the same list.
    12.5  *}
    12.6  
    12.7 -ML_setup {*
    12.8 +ML {*
    12.9  local
   12.10  
   12.11  fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
    13.1 --- a/src/HOL/OrderedGroup.thy	Sat Mar 29 19:13:58 2008 +0100
    13.2 +++ b/src/HOL/OrderedGroup.thy	Sat Mar 29 19:14:00 2008 +0100
    13.3 @@ -1421,7 +1421,7 @@
    13.4  end);
    13.5  *}
    13.6  
    13.7 -ML_setup {*
    13.8 +ML {*
    13.9    Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
   13.10  *}
   13.11  
    14.1 --- a/src/HOL/Product_Type.thy	Sat Mar 29 19:13:58 2008 +0100
    14.2 +++ b/src/HOL/Product_Type.thy	Sat Mar 29 19:14:00 2008 +0100
    14.3 @@ -57,7 +57,7 @@
    14.4    this rule directly --- it loops!
    14.5  *}
    14.6  
    14.7 -ML_setup {*
    14.8 +ML {*
    14.9    val unit_eq_proc =
   14.10      let val unit_meta_eq = mk_meta_eq @{thm unit_eq} in
   14.11        Simplifier.simproc @{theory} "unit_eq" ["x::unit"]
   14.12 @@ -323,7 +323,7 @@
   14.13  
   14.14  lemmas split_tupled_all = split_paired_all unit_all_eq2
   14.15  
   14.16 -ML_setup {*
   14.17 +ML {*
   14.18    (* replace parameters of product type by individual component parameters *)
   14.19    val safe_full_simp_tac = generic_simp_tac true (true, false, false);
   14.20    local (* filtering with exists_paired_all is an essential optimization *)
   14.21 @@ -429,7 +429,7 @@
   14.22    split_beta}.
   14.23  *}
   14.24  
   14.25 -ML_setup {*
   14.26 +ML {*
   14.27  
   14.28  local
   14.29    val cond_split_eta_ss = HOL_basic_ss addsimps [thm "cond_split_eta"]
    15.1 --- a/src/HOL/Set.thy	Sat Mar 29 19:13:58 2008 +0100
    15.2 +++ b/src/HOL/Set.thy	Sat Mar 29 19:14:00 2008 +0100
    15.3 @@ -473,7 +473,7 @@
    15.4  lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"
    15.5    by blast
    15.6  
    15.7 -ML_setup {*
    15.8 +ML {*
    15.9    local
   15.10      val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
   15.11      fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    16.1 --- a/src/HOL/ex/Lagrange.thy	Sat Mar 29 19:13:58 2008 +0100
    16.2 +++ b/src/HOL/ex/Lagrange.thy	Sat Mar 29 19:14:00 2008 +0100
    16.3 @@ -25,7 +25,7 @@
    16.4  
    16.5  (* These two simprocs are even less efficient than ordered rewriting
    16.6     and kill the second example: *)
    16.7 -ML_setup {*
    16.8 +ML {*
    16.9    Delsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
   16.10  *}
   16.11  
    17.1 --- a/src/HOLCF/Pcpo.thy	Sat Mar 29 19:13:58 2008 +0100
    17.2 +++ b/src/HOLCF/Pcpo.thy	Sat Mar 29 19:14:00 2008 +0100
    17.3 @@ -197,7 +197,7 @@
    17.4  lemma UU_reorient: "(\<bottom> = x) = (x = \<bottom>)"
    17.5  by auto
    17.6  
    17.7 -ML_setup {*
    17.8 +ML {*
    17.9  local
   17.10    val meta_UU_reorient = thm "UU_reorient" RS eq_reflection;
   17.11    fun reorient_proc sg _ (_ $ t $ u) =
    18.1 --- a/src/Sequents/Washing.thy	Sat Mar 29 19:13:58 2008 +0100
    18.2 +++ b/src/Sequents/Washing.thy	Sat Mar 29 19:14:00 2008 +0100
    18.3 @@ -35,10 +35,10 @@
    18.4  
    18.5  (* "activate" definitions for use in proof *)
    18.6  
    18.7 -ML_setup {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *}
    18.8 -ML_setup {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *}
    18.9 -ML_setup {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *}
   18.10 -ML_setup {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *}
   18.11 +ML {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *}
   18.12 +ML {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *}
   18.13 +ML {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *}
   18.14 +ML {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *}
   18.15  
   18.16  (* a load of dirty clothes and two dollars gives you clean clothes *)
   18.17  
    19.1 --- a/src/ZF/Datatype_ZF.thy	Sat Mar 29 19:13:58 2008 +0100
    19.2 +++ b/src/ZF/Datatype_ZF.thy	Sat Mar 29 19:14:00 2008 +0100
    19.3 @@ -12,7 +12,7 @@
    19.4  uses "Tools/datatype_package.ML"
    19.5  begin
    19.6  
    19.7 -ML_setup {*
    19.8 +ML {*
    19.9  (*Typechecking rules for most datatypes involving univ*)
   19.10  structure Data_Arg =
   19.11    struct
    20.1 --- a/src/ZF/Inductive_ZF.thy	Sat Mar 29 19:13:58 2008 +0100
    20.2 +++ b/src/ZF/Inductive_ZF.thy	Sat Mar 29 19:14:00 2008 +0100
    20.3 @@ -41,7 +41,7 @@
    20.4  setup IndCases.setup
    20.5  setup DatatypeTactics.setup
    20.6  
    20.7 -ML_setup {*
    20.8 +ML {*
    20.9  structure Lfp =
   20.10    struct
   20.11    val oper      = @{const lfp}
    21.1 --- a/src/ZF/OrdQuant.thy	Sat Mar 29 19:13:58 2008 +0100
    21.2 +++ b/src/ZF/OrdQuant.thy	Sat Mar 29 19:14:00 2008 +0100
    21.3 @@ -369,7 +369,7 @@
    21.4  
    21.5  text {* Setting up the one-point-rule simproc *}
    21.6  
    21.7 -ML_setup {*
    21.8 +ML {*
    21.9  local
   21.10  
   21.11  val unfold_rex_tac = unfold_tac [@{thm rex_def}];