renamed NamedThmsFun to Named_Thms;
simplified/unified names of instances of Named_Thms;
--- a/src/CCL/Wfd.thy Thu Jul 02 17:33:36 2009 +0200
+++ b/src/CCL/Wfd.thy Thu Jul 02 17:34:14 2009 +0200
@@ -495,7 +495,7 @@
ML {*
local
- structure Data = NamedThmsFun(val name = "eval" val description = "evaluation rules");
+ structure Data = Named_Thms(val name = "eval" val description = "evaluation rules");
in
fun eval_tac ctxt ths =
--- a/src/HOL/Deriv.thy Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Deriv.thy Thu Jul 02 17:34:14 2009 +0200
@@ -315,14 +315,14 @@
text {* @{text "DERIV_intros"} *}
ML {*
-structure DerivIntros = NamedThmsFun
+structure Deriv_Intros = Named_Thms
(
val name = "DERIV_intros"
val description = "DERIV introduction rules"
)
*}
-setup DerivIntros.setup
+setup Deriv_Intros.setup
lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = Y \<rbrakk> \<Longrightarrow> DERIV f x :> Y"
by simp
--- a/src/HOL/HOL.thy Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/HOL.thy Thu Jul 02 17:34:14 2009 +0200
@@ -923,9 +923,11 @@
ML_Antiquote.value "claset"
(Scan.succeed "Classical.local_claset_of (ML_Context.the_local_context ())");
-structure ResAtpset = NamedThmsFun(val name = "atp" val description = "ATP rules");
+structure ResAtpset = Named_Thms
+ (val name = "atp" val description = "ATP rules");
-structure ResBlacklist = NamedThmsFun(val name = "noatp" val description = "theorems blacklisted for ATP");
+structure ResBlacklist = Named_Thms
+ (val name = "noatp" val description = "theorems blacklisted for ATP");
*}
text {*ResBlacklist holds theorems blacklisted to sledgehammer.
@@ -1982,19 +1984,18 @@
Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
*} "solve goal by normalization"
+
subsubsection {* Quickcheck *}
ML {*
-structure Quickcheck_RecFun_Simp_Thms = NamedThmsFun
+structure Quickcheck_RecFun_Simps = Named_Thms
(
val name = "quickcheck_recfun_simp"
val description = "simplification rules of recursive functions as needed by Quickcheck"
)
*}
-setup {*
- Quickcheck_RecFun_Simp_Thms.setup
-*}
+setup Quickcheck_RecFun_Simps.setup
setup {*
Quickcheck.add_generator ("SML", Codegen.test_term)
@@ -2008,22 +2009,22 @@
text {* This will be relocated once Nitpick is moved to HOL. *}
ML {*
-structure Nitpick_Const_Def_Thms = NamedThmsFun
+structure Nitpick_Const_Defs = Named_Thms
(
val name = "nitpick_const_def"
val description = "alternative definitions of constants as needed by Nitpick"
)
-structure Nitpick_Const_Simp_Thms = NamedThmsFun
+structure Nitpick_Const_Simps = Named_Thms
(
val name = "nitpick_const_simp"
val description = "equational specification of constants as needed by Nitpick"
)
-structure Nitpick_Const_Psimp_Thms = NamedThmsFun
+structure Nitpick_Const_Psimps = Named_Thms
(
val name = "nitpick_const_psimp"
val description = "partial equational specification of constants as needed by Nitpick"
)
-structure Nitpick_Ind_Intro_Thms = NamedThmsFun
+structure Nitpick_Ind_Intros = Named_Thms
(
val name = "nitpick_ind_intro"
val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
@@ -2031,10 +2032,10 @@
*}
setup {*
- Nitpick_Const_Def_Thms.setup
- #> Nitpick_Const_Simp_Thms.setup
- #> Nitpick_Const_Psimp_Thms.setup
- #> Nitpick_Ind_Intro_Thms.setup
+ Nitpick_Const_Defs.setup
+ #> Nitpick_Const_Simps.setup
+ #> Nitpick_Const_Psimps.setup
+ #> Nitpick_Ind_Intros.setup
*}
--- a/src/HOL/Limits.thy Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Limits.thy Thu Jul 02 17:34:14 2009 +0200
@@ -350,7 +350,7 @@
lemmas Zfun_mult_left = mult.Zfun_left
-subsection{* Limits *}
+subsection {* Limits *}
definition
tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
@@ -358,13 +358,15 @@
where [code del]:
"(f ---> l) net \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
-ML{*
-structure TendstoIntros =
- NamedThmsFun(val name = "tendsto_intros"
- val description = "introduction rules for tendsto");
+ML {*
+structure Tendsto_Intros = Named_Thms
+(
+ val name = "tendsto_intros"
+ val description = "introduction rules for tendsto"
+)
*}
-setup TendstoIntros.setup
+setup Tendsto_Intros.setup
lemma topological_tendstoI:
"(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
--- a/src/HOL/Nominal/nominal_primrec.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Thu Jul 02 17:34:14 2009 +0200
@@ -373,7 +373,7 @@
lthy''
|> LocalTheory.note Thm.generatedK ((qualify (Binding.name "simps"),
map (Attrib.internal o K)
- [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]),
+ [Simplifier.simp_add, Nitpick_Const_Simps.add]),
maps snd simps')
|> snd
end)
--- a/src/HOL/OrderedGroup.thy Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/OrderedGroup.thy Thu Jul 02 17:34:14 2009 +0200
@@ -22,13 +22,15 @@
\end{itemize}
*}
-ML{*
-structure AlgebraSimps =
- NamedThmsFun(val name = "algebra_simps"
- val description = "algebra simplification rules");
+ML {*
+structure Algebra_Simps = Named_Thms
+(
+ val name = "algebra_simps"
+ val description = "algebra simplification rules"
+)
*}
-setup AlgebraSimps.setup
+setup Algebra_Simps.setup
text{* The rewrites accumulated in @{text algebra_simps} deal with the
classical algebraic structures of groups, rings and family. They simplify
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Jul 02 17:34:14 2009 +0200
@@ -264,7 +264,7 @@
thy2
|> Sign.add_path (space_implode "_" new_type_names)
|> PureThy.add_thmss [((Binding.name "recs", rec_thms),
- [Nitpick_Const_Simp_Thms.add])]
+ [Nitpick_Const_Simps.add])]
||> Sign.parent_path
||> Theory.checkpoint
|-> (fn thms => pair (reccomb_names, Library.flat thms))
@@ -337,7 +337,7 @@
(DatatypeProp.make_cases new_type_names descr sorts thy2)
in
thy2
- |> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms
+ |> Context.the_theory o fold (fold Nitpick_Const_Simps.add_thm) case_thms
o Context.Theory
|> parent_path (#flat_names config)
|> store_thmss "cases" new_type_names case_thms
--- a/src/HOL/Tools/Function/fundef.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/Function/fundef.ML Thu Jul 02 17:34:14 2009 +0200
@@ -37,12 +37,12 @@
val simp_attribs = map (Attrib.internal o K)
[Simplifier.simp_add,
Code.add_default_eqn_attribute,
- Nitpick_Const_Simp_Thms.add,
- Quickcheck_RecFun_Simp_Thms.add]
+ Nitpick_Const_Simps.add,
+ Quickcheck_RecFun_Simps.add]
val psimp_attribs = map (Attrib.internal o K)
[Simplifier.simp_add,
- Nitpick_Const_Psimp_Thms.add]
+ Nitpick_Const_Psimps.add]
fun note_theorem ((name, atts), ths) =
LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths)
@@ -202,7 +202,7 @@
"declaration of congruence rule for function definitions"
#> setup_case_cong
#> FundefRelation.setup
- #> FundefCommon.TerminationSimps.setup
+ #> FundefCommon.Termination_Simps.setup
val get_congs = FundefCtxTree.get_fundef_congs
--- a/src/HOL/Tools/Function/fundef_common.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_common.ML Thu Jul 02 17:34:14 2009 +0200
@@ -144,7 +144,7 @@
(* Simp rules for termination proofs *)
-structure TerminationSimps = NamedThmsFun
+structure Termination_Simps = Named_Thms
(
val name = "termination_simp"
val description = "Simplification rule for termination proofs"
--- a/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 02 17:34:14 2009 +0200
@@ -216,7 +216,8 @@
fun lexicographic_order_tac ctxt =
TRY (FundefCommon.apply_termination_rule ctxt 1)
- THEN lex_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt))
+ THEN lex_order_tac ctxt
+ (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.Termination_Simps.get ctxt))
val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac
--- a/src/HOL/Tools/Function/measure_functions.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/Function/measure_functions.ML Thu Jul 02 17:34:14 2009 +0200
@@ -1,7 +1,7 @@
(* Title: HOL/Tools/Function/measure_functions.ML
Author: Alexander Krauss, TU Muenchen
-Measure functions, generated heuristically
+Measure functions, generated heuristically.
*)
signature MEASURE_FUNCTIONS =
@@ -16,7 +16,8 @@
struct
(** User-declared size functions **)
-structure MeasureHeuristicRules = NamedThmsFun(
+structure Measure_Heuristic_Rules = Named_Thms
+(
val name = "measure_function"
val description = "Rules that guide the heuristic generation of measure functions"
);
@@ -24,7 +25,7 @@
fun mk_is_measures t = Const (@{const_name "is_measure"}, fastype_of t --> HOLogic.boolT) $ t
fun find_measures ctxt T =
- DEPTH_SOLVE (resolve_tac (MeasureHeuristicRules.get ctxt) 1)
+ DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1)
(HOLogic.mk_Trueprop (mk_is_measures (Var (("f",0), T --> HOLogic.natT)))
|> cterm_of (ProofContext.theory_of ctxt) |> Goal.init)
|> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
@@ -41,7 +42,7 @@
@ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
| mk_funorder_funs T = [ constant_1 T ]
-fun mk_ext_base_funs ctxt (Type("+", [fT, sT])) =
+fun mk_ext_base_funs ctxt (Type ("+", [fT, sT])) =
map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
(mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
| mk_ext_base_funs ctxt T = find_measures ctxt T
@@ -52,7 +53,7 @@
val get_measure_functions = mk_all_measure_funs
-val setup = MeasureHeuristicRules.setup
+val setup = Measure_Heuristic_Rules.setup
end
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Jul 02 17:34:14 2009 +0200
@@ -405,7 +405,7 @@
fun decomp_scnp orders ctxt =
let
- val extra_simps = FundefCommon.TerminationSimps.get ctxt
+ val extra_simps = FundefCommon.Termination_Simps.get ctxt
val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps)
in
SIMPLE_METHOD
--- a/src/HOL/Tools/Function/size.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/Function/size.ML Thu Jul 02 17:34:14 2009 +0200
@@ -209,7 +209,7 @@
val ([size_thms], thy'') = PureThy.add_thmss
[((Binding.name "size", size_eqns),
- [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
+ [Simplifier.simp_add, Nitpick_Const_Simps.add,
Thm.declaration_attribute
(fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
--- a/src/HOL/Tools/arith_data.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/arith_data.ML Thu Jul 02 17:34:14 2009 +0200
@@ -28,7 +28,8 @@
(* slots for plugging in arithmetic facts and tactics *)
-structure Arith_Facts = NamedThmsFun(
+structure Arith_Facts = Named_Thms
+(
val name = "arith"
val description = "arith facts - only ground formulas"
);
--- a/src/HOL/Tools/inductive.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/inductive.ML Thu Jul 02 17:34:14 2009 +0200
@@ -694,7 +694,7 @@
LocalTheory.notes kind
(map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
[Attrib.internal (K (ContextRules.intro_query NONE)),
- Attrib.internal (K Nitpick_Ind_Intro_Thms.add)])]) intrs) |>>
+ Attrib.internal (K Nitpick_Ind_Intros.add)])]) intrs) |>>
map (hd o snd);
val (((_, elims'), (_, [induct'])), ctxt2) =
ctxt1 |>
--- a/src/HOL/Tools/old_primrec.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML Thu Jul 02 17:34:14 2009 +0200
@@ -283,8 +283,8 @@
val simps'' = maps snd simps';
in
thy''
- |> note (("simps", [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
- Code.add_default_eqn_attribute]), simps'')
+ |> note (("simps",
+ [Simplifier.simp_add, Nitpick_Const_Simps.add, Code.add_default_eqn_attribute]), simps'')
|> snd
|> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
|> snd
--- a/src/HOL/Tools/primrec.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/primrec.ML Thu Jul 02 17:34:14 2009 +0200
@@ -272,7 +272,7 @@
(Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec;
fun simp_attr_binding prefix = (Binding.qualify true prefix (Binding.name "simps"),
map (Attrib.internal o K)
- [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]);
+ [Simplifier.simp_add, Nitpick_Const_Simps.add, Quickcheck_RecFun_Simps.add]);
in
lthy
|> set_group ? LocalTheory.set_group (serial_string ())
--- a/src/HOL/Tools/quickcheck_generators.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Thu Jul 02 17:34:14 2009 +0200
@@ -244,7 +244,7 @@
|-> (fn proto_simps => prove_simps proto_simps)
|-> (fn simps => LocalTheory.note Thm.generatedK ((b,
Code.add_default_eqn_attrib :: map (Attrib.internal o K)
- [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]),
+ [Simplifier.simp_add, Nitpick_Const_Simps.add, Quickcheck_RecFun_Simps.add]),
simps))
|> snd
end
--- a/src/HOL/Tools/recdef.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/recdef.ML Thu Jul 02 17:34:14 2009 +0200
@@ -207,8 +207,8 @@
tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
congs wfs name R eqs;
val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
- val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
- Code.add_default_eqn_attribute, Quickcheck_RecFun_Simp_Thms.add] else [];
+ val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simps.add,
+ Code.add_default_eqn_attribute, Quickcheck_RecFun_Simps.add] else [];
val ((simps' :: rules', [induct']), thy) =
thy
--- a/src/HOL/Tools/record.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/record.ML Thu Jul 02 17:34:14 2009 +0200
@@ -2192,7 +2192,7 @@
thms_thy
|> (snd oo PureThy.add_thmss)
[((Binding.name "simps", sel_upd_simps),
- [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]),
+ [Simplifier.simp_add, Nitpick_Const_Simps.add]),
((Binding.name "iffs", iffs), [iff_add])]
|> put_record name (make_record_info args parent fields extension induct_scheme')
|> put_sel_upd (names @ [full_moreN]) sel_upd_simps
--- a/src/HOL/ex/Numeral.thy Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/ex/Numeral.thy Thu Jul 02 17:34:14 2009 +0200
@@ -93,11 +93,14 @@
subsection {* Numeral operations *}
ML {*
-structure DigSimps =
- NamedThmsFun(val name = "numeral"; val description = "Simplification rules for numerals")
+structure Dig_Simps = Named_Thms
+(
+ val name = "numeral"
+ val description = "Simplification rules for numerals"
+)
*}
-setup DigSimps.setup
+setup Dig_Simps.setup
instantiation num :: "{plus,times,ord}"
begin
--- a/src/HOLCF/Cont.thy Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOLCF/Cont.thy Thu Jul 02 17:34:14 2009 +0200
@@ -140,8 +140,11 @@
subsection {* Continuity simproc *}
ML {*
-structure Cont2ContData = NamedThmsFun
- ( val name = "cont2cont" val description = "continuity intro rule" )
+structure Cont2ContData = Named_Thms
+(
+ val name = "cont2cont"
+ val description = "continuity intro rule"
+)
*}
setup Cont2ContData.setup
--- a/src/Tools/atomize_elim.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/Tools/atomize_elim.ML Thu Jul 02 17:34:14 2009 +0200
@@ -20,7 +20,9 @@
struct
(* theory data *)
-structure AtomizeElimData = NamedThmsFun(
+
+structure AtomizeElimData = Named_Thms
+(
val name = "atomize_elim";
val description = "atomize_elim rewrite rule";
);
--- a/src/ZF/UNITY/Constrains.thy Thu Jul 02 17:33:36 2009 +0200
+++ b/src/ZF/UNITY/Constrains.thy Thu Jul 02 17:34:14 2009 +0200
@@ -462,7 +462,11 @@
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I});
(*To allow expansion of the program's definition when appropriate*)
-structure ProgramDefs = NamedThmsFun(val name = "program" val description = "program definitions");
+structure Program_Defs = Named_Thms
+(
+ val name = "program"
+ val description = "program definitions"
+);
(*proves "co" properties when the program is specified*)
@@ -478,7 +482,7 @@
(* Three subgoals *)
rewrite_goal_tac [@{thm st_set_def}] 3,
REPEAT (force_tac css 2),
- full_simp_tac (ss addsimps (ProgramDefs.get ctxt)) 1,
+ full_simp_tac (ss addsimps (Program_Defs.get ctxt)) 1,
ALLGOALS (clarify_tac cs),
REPEAT (FIRSTGOAL (etac disjE)),
ALLGOALS (clarify_tac cs),
@@ -493,7 +497,7 @@
rtac @{thm AlwaysI} i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i;
*}
-setup ProgramDefs.setup
+setup Program_Defs.setup
method_setup safety = {*
Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
--- a/src/ZF/UNITY/SubstAx.thy Thu Jul 02 17:33:36 2009 +0200
+++ b/src/ZF/UNITY/SubstAx.thy Thu Jul 02 17:34:14 2009 +0200
@@ -359,7 +359,7 @@
REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
@{thm EnsuresI}, @{thm ensuresI}] 1),
(*now there are two subgoals: co & transient*)
- simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2,
+ simp_tac (ss addsimps (Program_Defs.get ctxt)) 2,
res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
(*simplify the command's domain*)
simp_tac (ss addsimps [@{thm domain_def}]) 3,