Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Drule.norm_hhf_eqs;
authorwenzelm
Thu, 16 Oct 2008 22:44:29 +0200
changeset 28620 9846d772b306
parent 28619 89f9dd800a22
child 28621 a60164e8fff0
Drule.norm_hhf_eqs;
src/Pure/Isar/object_logic.ML file | annotate | diff | comparison | revisions
src/Pure/meta_simplifier.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/object_logic.ML	Thu Oct 16 22:44:28 2008 +0200
+++ b/src/Pure/Isar/object_logic.ML	Thu Oct 16 22:44:29 2008 +0200
@@ -193,7 +193,7 @@
 val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
 val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
 
-val _ = Context.>> (Context.map_theory (add_rulify Drule.norm_hhf_eq));
+val _ = Context.>> (Context.map_theory (fold add_rulify Drule.norm_hhf_eqs));
 
 
 (* atomize *)
--- a/src/Pure/meta_simplifier.ML	Thu Oct 16 22:44:28 2008 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu Oct 16 22:44:29 2008 +0200
@@ -1344,7 +1344,7 @@
   |> Thm.adjust_maxidx_thm ~1
   |> Drule.gen_all;
 
-val hhf_ss = empty_ss addsimps [Drule.norm_hhf_eq];
+val hhf_ss = empty_ss addsimps Drule.norm_hhf_eqs;
 
 in
isabelle