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.
RuleCases.case_conclusion;
authorwenzelm
Wed, 23 Nov 2005 18:52:01 +0100
changeset 18234 0183318232f2
parent 18233 5a124c76e92f
child 18235 63da52e2d6dc
RuleCases.case_conclusion;
src/HOL/Tools/inductive_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/inductive_package.ML	Wed Nov 23 18:52:00 2005 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Wed Nov 23 18:52:01 2005 +0100
@@ -788,7 +788,7 @@
     val induct =
       if coind then
         (raw_induct, [RuleCases.case_names [rec_name],
-          RuleCases.case_conclusion_binops rec_name induct_cases,
+          RuleCases.case_conclusion (rec_name, induct_cases),
           RuleCases.consumes 1])
       else if no_ind orelse length cs > 1 then
         (raw_induct, [RuleCases.case_names induct_cases, RuleCases.consumes 0])
isabelle