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.
Changed interface of add_inductive: monos and con_defs are now
authorberghofe
Wed, 21 Oct 1998 17:52:38 +0200
changeset 5718 e5094d678285
parent 5717 0d28dbe484b6
child 5719 2aed60cdb9f2
Changed interface of add_inductive: monos and con_defs are now lists of xstrings.
src/HOL/Tools/inductive_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/inductive_package.ML	Wed Oct 21 17:48:02 1998 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Wed Oct 21 17:52:38 1998 +0200
@@ -37,7 +37,7 @@
        mk_cases:thm list -> string -> thm, mono:thm,
        unfold:thm}
   val add_inductive : bool -> bool -> string list -> string list
-    -> thm list -> thm list -> theory -> theory *
+    -> xstring list -> xstring list -> theory -> theory *
       {defs:thm list, elims:thm list, raw_induct:thm, induct:thm,
        intrs:thm list,
        mk_cases:thm list -> string -> thm, mono:thm,
@@ -600,7 +600,8 @@
     val intr_ts'' = map subst intr_ts';
 
   in add_inductive_i verbose false "" coind false false cs'' intr_ts''
-    monos con_defs thy
+    (map (Attribute.thm_of) (PureThy.get_tthmss thy monos))
+    (map (Attribute.thm_of) (PureThy.get_tthmss thy con_defs)) thy
   end;
 
 end;
isabelle