tuned;
authorwenzelm
Tue May 31 11:53:12 2005 +0200 (2005-05-31)
changeset 16121a80aa66d2271
parent 16120 6a449deff8d9
child 16122 864fda4a4056
tuned;
src/FOL/IFOL.thy
src/HOL/Bali/AxExample.thy
src/HOL/Bali/Basis.thy
src/HOL/Extraction.thy
src/HOL/HOL.thy
src/HOL/Orderings.thy
src/HOL/Product_Type.thy
src/HOLCF/Domain.thy
src/HOLCF/Lift.thy
src/HOLCF/Tr.thy
     1.1 --- a/src/FOL/IFOL.thy	Tue May 31 11:53:11 2005 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Tue May 31 11:53:12 2005 +0200
     1.3 @@ -184,8 +184,8 @@
     1.4    and [Pure.elim 2] = allE notE' impE'
     1.5    and [Pure.intro] = exI disjI2 disjI1
     1.6  
     1.7 -ML_setup {*
     1.8 -  Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac));
     1.9 +setup {*
    1.10 +  [ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac)]
    1.11  *}
    1.12  
    1.13  
     2.1 --- a/src/HOL/Bali/AxExample.thy	Tue May 31 11:53:11 2005 +0200
     2.2 +++ b/src/HOL/Bali/AxExample.thy	Tue May 31 11:53:12 2005 +0200
     2.3 @@ -39,7 +39,7 @@
     2.4  declare split_if_asm [split del]
     2.5  declare lvar_def [simp]
     2.6  
     2.7 -ML_setup {*
     2.8 +ML {*
     2.9  fun inst1_tac s t st = case assoc (rev (term_varnames (prop_of st)), s) of
    2.10    SOME i => Tactic.instantiate_tac' [((s, i), t)] st | NONE => Seq.empty;
    2.11  val ax_tac = REPEAT o rtac allI THEN'
     3.1 --- a/src/HOL/Bali/Basis.thy	Tue May 31 11:53:11 2005 +0200
     3.2 +++ b/src/HOL/Bali/Basis.thy	Tue May 31 11:53:12 2005 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  
     3.5  theory Basis = Main:
     3.6  
     3.7 -ML_setup {*
     3.8 +ML {*
     3.9  Unify.search_bound := 40;
    3.10  Unify.trace_bound  := 40;
    3.11  *}
     4.1 --- a/src/HOL/Extraction.thy	Tue May 31 11:53:11 2005 +0200
     4.2 +++ b/src/HOL/Extraction.thy	Tue May 31 11:53:12 2005 +0200
     4.3 @@ -12,7 +12,8 @@
     4.4  
     4.5  subsection {* Setup *}
     4.6  
     4.7 -ML_setup {*
     4.8 +setup {*
     4.9 +let
    4.10  fun realizes_set_proc (Const ("realizes", Type ("fun", [Type ("Null", []), _])) $ r $
    4.11        (Const ("op :", _) $ x $ S)) = (case strip_comb S of
    4.12          (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, binder_types U @
    4.13 @@ -33,18 +34,18 @@
    4.14    Abs ("x", elT, Const ("realizes", rT --> HOLogic.boolT --> HOLogic.boolT) $
    4.15      incr_boundvars 1 r $ (Const ("op :", elT --> setT --> HOLogic.boolT) $
    4.16        Bound 0 $ incr_boundvars 1 s));
    4.17 -
    4.18 -  Context.>> (fn thy => thy |>
    4.19 -    Extraction.add_types
    4.20 +in
    4.21 +  [Extraction.add_types
    4.22        [("bool", ([], NONE)),
    4.23 -       ("set", ([realizes_set_proc], SOME mk_realizes_set))] |>
    4.24 +       ("set", ([realizes_set_proc], SOME mk_realizes_set))],
    4.25      Extraction.set_preprocessor (fn sg =>
    4.26        Proofterm.rewrite_proof_notypes
    4.27          ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) ::
    4.28            ProofRewriteRules.rprocs true) o
    4.29        Proofterm.rewrite_proof (Sign.tsig_of sg)
    4.30          (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
    4.31 -      ProofRewriteRules.elim_vars (curry Const "arbitrary")))
    4.32 +      ProofRewriteRules.elim_vars (curry Const "arbitrary"))]
    4.33 +end
    4.34  *}
    4.35  
    4.36  lemmas [extraction_expand] =
     5.1 --- a/src/HOL/HOL.thy	Tue May 31 11:53:11 2005 +0200
     5.2 +++ b/src/HOL/HOL.thy	Tue May 31 11:53:12 2005 +0200
     5.3 @@ -899,8 +899,8 @@
     5.4  use "cladata.ML"
     5.5  setup hypsubst_setup
     5.6  
     5.7 -ML_setup {*
     5.8 -  Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac));
     5.9 +setup {*
    5.10 +  [ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)]
    5.11  *}
    5.12  
    5.13  setup Classical.setup
     6.1 --- a/src/HOL/Orderings.thy	Tue May 31 11:53:11 2005 +0200
     6.2 +++ b/src/HOL/Orderings.thy	Tue May 31 11:53:12 2005 +0200
     6.3 @@ -384,7 +384,6 @@
     6.4  
     6.5  interpretation min_max:
     6.6    lower_semilattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
     6.7 -apply -
     6.8  apply(rule lower_semilattice_axioms.intro)
     6.9  apply(simp add:min_def linorder_not_le order_less_imp_le)
    6.10  apply(simp add:min_def linorder_not_le order_less_imp_le)
     7.1 --- a/src/HOL/Product_Type.thy	Tue May 31 11:53:11 2005 +0200
     7.2 +++ b/src/HOL/Product_Type.thy	Tue May 31 11:53:12 2005 +0200
     7.3 @@ -258,7 +258,7 @@
     7.4  lemma PairE [cases type: *]: "(!!x y. p = (x, y) ==> Q) ==> Q"
     7.5    by (insert PairE_lemma [of p]) blast
     7.6  
     7.7 -ML_setup {*
     7.8 +ML {*
     7.9    local val PairE = thm "PairE" in
    7.10      fun pair_tac s =
    7.11        EVERY' [res_inst_tac [("p", s)] PairE, hyp_subst_tac, K prune_params_tac];
    7.12 @@ -298,17 +298,17 @@
    7.13    ?P(a, b)"} which cannot be solved by reflexivity.
    7.14  *}
    7.15  
    7.16 -ML_setup "
    7.17 +ML_setup {*
    7.18    (* replace parameters of product type by individual component parameters *)
    7.19    val safe_full_simp_tac = generic_simp_tac true (true, false, false);
    7.20    local (* filtering with exists_paired_all is an essential optimization *)
    7.21 -    fun exists_paired_all (Const (\"all\", _) $ Abs (_, T, t)) =
    7.22 +    fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) =
    7.23            can HOLogic.dest_prodT T orelse exists_paired_all t
    7.24        | exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u
    7.25        | exists_paired_all (Abs (_, _, t)) = exists_paired_all t
    7.26        | exists_paired_all _ = false;
    7.27      val ss = HOL_basic_ss
    7.28 -      addsimps [thm \"split_paired_all\", thm \"unit_all_eq2\", thm \"unit_abs_eta_conv\"]
    7.29 +      addsimps [thm "split_paired_all", thm "unit_all_eq2", thm "unit_abs_eta_conv"]
    7.30        addsimprocs [unit_eq_proc];
    7.31    in
    7.32      val split_all_tac = SUBGOAL (fn (t, i) =>
    7.33 @@ -319,8 +319,8 @@
    7.34     if exists_paired_all (#prop (Thm.rep_thm th)) then full_simplify ss th else th;
    7.35    end;
    7.36  
    7.37 -claset_ref() := claset() addSbefore (\"split_all_tac\", split_all_tac);
    7.38 -"
    7.39 +claset_ref() := claset() addSbefore ("split_all_tac", split_all_tac);
    7.40 +*}
    7.41  
    7.42  lemma split_paired_All [simp]: "(ALL x. P x) = (ALL a b. P (a, b))"
    7.43    -- {* @{text "[iff]"} is not a good idea because it makes @{text blast} loop *}
    7.44 @@ -515,21 +515,21 @@
    7.45  declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
    7.46  declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
    7.47  
    7.48 -ML_setup "
    7.49 +ML_setup {*
    7.50  local (* filtering with exists_p_split is an essential optimization *)
    7.51 -  fun exists_p_split (Const (\"split\",_) $ _ $ (Const (\"Pair\",_)$_$_)) = true
    7.52 +  fun exists_p_split (Const ("split",_) $ _ $ (Const ("Pair",_)$_$_)) = true
    7.53      | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
    7.54      | exists_p_split (Abs (_, _, t)) = exists_p_split t
    7.55      | exists_p_split _ = false;
    7.56 -  val ss = HOL_basic_ss addsimps [thm \"split_conv\"];
    7.57 +  val ss = HOL_basic_ss addsimps [thm "split_conv"];
    7.58  in
    7.59  val split_conv_tac = SUBGOAL (fn (t, i) =>
    7.60      if exists_p_split t then safe_full_simp_tac ss i else no_tac);
    7.61  end;
    7.62  (* This prevents applications of splitE for already splitted arguments leading
    7.63     to quite time-consuming computations (in particular for nested tuples) *)
    7.64 -claset_ref() := claset() addSbefore (\"split_conv_tac\", split_conv_tac);
    7.65 -"
    7.66 +claset_ref() := claset() addSbefore ("split_conv_tac", split_conv_tac);
    7.67 +*}
    7.68  
    7.69  lemma split_eta_SetCompr [simp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
    7.70  by (rule ext, fast)
     8.1 --- a/src/HOLCF/Domain.thy	Tue May 31 11:53:11 2005 +0200
     8.2 +++ b/src/HOLCF/Domain.thy	Tue May 31 11:53:12 2005 +0200
     8.3 @@ -158,7 +158,7 @@
     8.4  
     8.5  subsection {* Setting up the package *}
     8.6  
     8.7 -ML_setup {*
     8.8 +ML {*
     8.9  val iso_intro       = thm "iso.intro";
    8.10  val iso_abs_iso     = thm "iso.abs_iso";
    8.11  val iso_rep_iso     = thm "iso.rep_iso";
     9.1 --- a/src/HOLCF/Lift.thy	Tue May 31 11:53:11 2005 +0200
     9.2 +++ b/src/HOLCF/Lift.thy	Tue May 31 11:53:12 2005 +0200
     9.3 @@ -165,7 +165,7 @@
     9.4    For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text
     9.5    x} by @{text "Def a"} in conclusion. *}
     9.6  
     9.7 -ML_setup {*
     9.8 +ML {*
     9.9    local val not_Undef_is_Def = thm "not_Undef_is_Def"
    9.10    in val def_tac = SIMPSET' (fn ss =>
    9.11      etac (not_Undef_is_Def RS iffD1 RS exE) THEN' asm_simp_tac ss)
    9.12 @@ -268,7 +268,7 @@
    9.13    cont_flift1_arg_and_not_arg cont2cont_CF1L_rev2
    9.14    cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if
    9.15  
    9.16 -ML_setup {*
    9.17 +ML {*
    9.18  val cont_lemmas2 = cont_lemmas1 @ thms "cont_lemmas_ext";
    9.19  
    9.20  fun cont_tac  i = resolve_tac cont_lemmas2 i;
    10.1 --- a/src/HOLCF/Tr.thy	Tue May 31 11:53:11 2005 +0200
    10.2 +++ b/src/HOLCF/Tr.thy	Tue May 31 11:53:12 2005 +0200
    10.3 @@ -132,7 +132,7 @@
    10.4  apply (simp_all)
    10.5  done
    10.6  
    10.7 -ML_setup {*
    10.8 +ML {*
    10.9  val split_If_tac =
   10.10    simp_tac (HOL_basic_ss addsimps [symmetric (thm "If2_def")])
   10.11      THEN' (split_tac [thm "split_If2"])