# HG changeset patch # User wenzelm # Date 1117533192 -7200 # Node ID a80aa66d2271d4e7de3b952d2f20499cb2125413 # Parent 6a449deff8d9dcc463645c093336b71d966617f5 tuned; diff -r 6a449deff8d9 -r a80aa66d2271 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Tue May 31 11:53:11 2005 +0200 +++ b/src/FOL/IFOL.thy Tue May 31 11:53:12 2005 +0200 @@ -184,8 +184,8 @@ and [Pure.elim 2] = allE notE' impE' and [Pure.intro] = exI disjI2 disjI1 -ML_setup {* - Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac)); +setup {* + [ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac)] *} diff -r 6a449deff8d9 -r a80aa66d2271 src/HOL/Bali/AxExample.thy --- a/src/HOL/Bali/AxExample.thy Tue May 31 11:53:11 2005 +0200 +++ b/src/HOL/Bali/AxExample.thy Tue May 31 11:53:12 2005 +0200 @@ -39,7 +39,7 @@ declare split_if_asm [split del] declare lvar_def [simp] -ML_setup {* +ML {* fun inst1_tac s t st = case assoc (rev (term_varnames (prop_of st)), s) of SOME i => Tactic.instantiate_tac' [((s, i), t)] st | NONE => Seq.empty; val ax_tac = REPEAT o rtac allI THEN' diff -r 6a449deff8d9 -r a80aa66d2271 src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Tue May 31 11:53:11 2005 +0200 +++ b/src/HOL/Bali/Basis.thy Tue May 31 11:53:12 2005 +0200 @@ -7,7 +7,7 @@ theory Basis = Main: -ML_setup {* +ML {* Unify.search_bound := 40; Unify.trace_bound := 40; *} diff -r 6a449deff8d9 -r a80aa66d2271 src/HOL/Extraction.thy --- a/src/HOL/Extraction.thy Tue May 31 11:53:11 2005 +0200 +++ b/src/HOL/Extraction.thy Tue May 31 11:53:12 2005 +0200 @@ -12,7 +12,8 @@ subsection {* Setup *} -ML_setup {* +setup {* +let fun realizes_set_proc (Const ("realizes", Type ("fun", [Type ("Null", []), _])) $ r $ (Const ("op :", _) $ x $ S)) = (case strip_comb S of (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, binder_types U @ @@ -33,18 +34,18 @@ Abs ("x", elT, Const ("realizes", rT --> HOLogic.boolT --> HOLogic.boolT) $ incr_boundvars 1 r $ (Const ("op :", elT --> setT --> HOLogic.boolT) $ Bound 0 $ incr_boundvars 1 s)); - - Context.>> (fn thy => thy |> - Extraction.add_types +in + [Extraction.add_types [("bool", ([], NONE)), - ("set", ([realizes_set_proc], SOME mk_realizes_set))] |> + ("set", ([realizes_set_proc], SOME mk_realizes_set))], Extraction.set_preprocessor (fn sg => Proofterm.rewrite_proof_notypes ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) :: ProofRewriteRules.rprocs true) o Proofterm.rewrite_proof (Sign.tsig_of sg) (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o - ProofRewriteRules.elim_vars (curry Const "arbitrary"))) + ProofRewriteRules.elim_vars (curry Const "arbitrary"))] +end *} lemmas [extraction_expand] = diff -r 6a449deff8d9 -r a80aa66d2271 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue May 31 11:53:11 2005 +0200 +++ b/src/HOL/HOL.thy Tue May 31 11:53:12 2005 +0200 @@ -899,8 +899,8 @@ use "cladata.ML" setup hypsubst_setup -ML_setup {* - Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)); +setup {* + [ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)] *} setup Classical.setup diff -r 6a449deff8d9 -r a80aa66d2271 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Tue May 31 11:53:11 2005 +0200 +++ b/src/HOL/Orderings.thy Tue May 31 11:53:12 2005 +0200 @@ -384,7 +384,6 @@ interpretation min_max: lower_semilattice["op \" "min :: 'a::linorder \ 'a \ 'a"] -apply - apply(rule lower_semilattice_axioms.intro) apply(simp add:min_def linorder_not_le order_less_imp_le) apply(simp add:min_def linorder_not_le order_less_imp_le) diff -r 6a449deff8d9 -r a80aa66d2271 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Tue May 31 11:53:11 2005 +0200 +++ b/src/HOL/Product_Type.thy Tue May 31 11:53:12 2005 +0200 @@ -258,7 +258,7 @@ lemma PairE [cases type: *]: "(!!x y. p = (x, y) ==> Q) ==> Q" by (insert PairE_lemma [of p]) blast -ML_setup {* +ML {* local val PairE = thm "PairE" in fun pair_tac s = EVERY' [res_inst_tac [("p", s)] PairE, hyp_subst_tac, K prune_params_tac]; @@ -298,17 +298,17 @@ ?P(a, b)"} which cannot be solved by reflexivity. *} -ML_setup " +ML_setup {* (* 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 *) - fun exists_paired_all (Const (\"all\", _) $ Abs (_, T, t)) = + fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) = can HOLogic.dest_prodT T orelse exists_paired_all t | exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u | exists_paired_all (Abs (_, _, t)) = exists_paired_all t | exists_paired_all _ = false; val ss = HOL_basic_ss - addsimps [thm \"split_paired_all\", thm \"unit_all_eq2\", thm \"unit_abs_eta_conv\"] + addsimps [thm "split_paired_all", thm "unit_all_eq2", thm "unit_abs_eta_conv"] addsimprocs [unit_eq_proc]; in val split_all_tac = SUBGOAL (fn (t, i) => @@ -319,8 +319,8 @@ if exists_paired_all (#prop (Thm.rep_thm th)) then full_simplify ss th else th; end; -claset_ref() := claset() addSbefore (\"split_all_tac\", split_all_tac); -" +claset_ref() := claset() addSbefore ("split_all_tac", split_all_tac); +*} lemma split_paired_All [simp]: "(ALL x. P x) = (ALL a b. P (a, b))" -- {* @{text "[iff]"} is not a good idea because it makes @{text blast} loop *} @@ -515,21 +515,21 @@ declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!] declare mem_splitE [elim!] splitE' [elim!] splitE [elim!] -ML_setup " +ML_setup {* local (* filtering with exists_p_split is an essential optimization *) - fun exists_p_split (Const (\"split\",_) $ _ $ (Const (\"Pair\",_)$_$_)) = true + fun exists_p_split (Const ("split",_) $ _ $ (Const ("Pair",_)$_$_)) = true | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u | exists_p_split (Abs (_, _, t)) = exists_p_split t | exists_p_split _ = false; - val ss = HOL_basic_ss addsimps [thm \"split_conv\"]; + val ss = HOL_basic_ss addsimps [thm "split_conv"]; in val split_conv_tac = SUBGOAL (fn (t, i) => if exists_p_split t then safe_full_simp_tac ss i else no_tac); end; (* This prevents applications of splitE for already splitted arguments leading to quite time-consuming computations (in particular for nested tuples) *) -claset_ref() := claset() addSbefore (\"split_conv_tac\", split_conv_tac); -" +claset_ref() := claset() addSbefore ("split_conv_tac", split_conv_tac); +*} lemma split_eta_SetCompr [simp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P" by (rule ext, fast) diff -r 6a449deff8d9 -r a80aa66d2271 src/HOLCF/Domain.thy --- a/src/HOLCF/Domain.thy Tue May 31 11:53:11 2005 +0200 +++ b/src/HOLCF/Domain.thy Tue May 31 11:53:12 2005 +0200 @@ -158,7 +158,7 @@ subsection {* Setting up the package *} -ML_setup {* +ML {* val iso_intro = thm "iso.intro"; val iso_abs_iso = thm "iso.abs_iso"; val iso_rep_iso = thm "iso.rep_iso"; diff -r 6a449deff8d9 -r a80aa66d2271 src/HOLCF/Lift.thy --- a/src/HOLCF/Lift.thy Tue May 31 11:53:11 2005 +0200 +++ b/src/HOLCF/Lift.thy Tue May 31 11:53:12 2005 +0200 @@ -165,7 +165,7 @@ For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text x} by @{text "Def a"} in conclusion. *} -ML_setup {* +ML {* local val not_Undef_is_Def = thm "not_Undef_is_Def" in val def_tac = SIMPSET' (fn ss => etac (not_Undef_is_Def RS iffD1 RS exE) THEN' asm_simp_tac ss) @@ -268,7 +268,7 @@ cont_flift1_arg_and_not_arg cont2cont_CF1L_rev2 cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if -ML_setup {* +ML {* val cont_lemmas2 = cont_lemmas1 @ thms "cont_lemmas_ext"; fun cont_tac i = resolve_tac cont_lemmas2 i; diff -r 6a449deff8d9 -r a80aa66d2271 src/HOLCF/Tr.thy --- a/src/HOLCF/Tr.thy Tue May 31 11:53:11 2005 +0200 +++ b/src/HOLCF/Tr.thy Tue May 31 11:53:12 2005 +0200 @@ -132,7 +132,7 @@ apply (simp_all) done -ML_setup {* +ML {* val split_If_tac = simp_tac (HOL_basic_ss addsimps [symmetric (thm "If2_def")]) THEN' (split_tac [thm "split_If2"])