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.
use of thm-antiquotation
authorChristian Urban <urbanc@in.tum.de>
Fri, 20 Nov 2009 00:20:32 +0100
changeset 33772 b6a1feca2ac2
parent 33771 17926df64f0f
child 33773 ccef2e6d8c21
use of thm-antiquotation
src/HOL/Nominal/nominal_inductive.ML file | annotate | diff | comparison | revisions
src/HOL/Nominal/nominal_inductive2.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Nov 19 16:07:53 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Nov 20 00:20:32 2009 +0100
@@ -15,9 +15,9 @@
 struct
 
 val inductive_forall_name = "HOL.induct_forall";
-val inductive_forall_def = thm "induct_forall_def";
-val inductive_atomize = thms "induct_atomize";
-val inductive_rulify = thms "induct_rulify";
+val inductive_forall_def = @{thm induct_forall_def};
+val inductive_atomize = @{thms induct_atomize};
+val inductive_rulify = @{thms induct_rulify};
 
 fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify [];
 
--- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Nov 19 16:07:53 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Nov 20 00:20:32 2009 +0100
@@ -15,9 +15,9 @@
 struct
 
 val inductive_forall_name = "HOL.induct_forall";
-val inductive_forall_def = thm "induct_forall_def";
-val inductive_atomize = thms "induct_atomize";
-val inductive_rulify = thms "induct_rulify";
+val inductive_forall_def = @{thm induct_forall_def};
+val inductive_atomize = @{thms induct_atomize};
+val inductive_rulify = @{thms induct_rulify};
 
 fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify [];
isabelle