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.
fixed case names in the weak induction principle and
authorurbanc
Fri, 28 Oct 2005 18:53:26 +0200
changeset 18017 f6abeac6dcb5
parent 18016 8f3a80033ba4
child 18018 82206a6c75c0
fixed case names in the weak induction principle and changed name from "induct" to "induct_weak"
src/HOL/Nominal/nominal_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nominal/nominal_package.ML	Fri Oct 28 18:22:26 2005 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Fri Oct 28 18:53:26 2005 +0200
@@ -1893,11 +1893,11 @@
             DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
                 (prems ~~ constr_defs))]));
 
-    val case_names_induct = mk_case_names_induct descr;
+    val case_names_induct = mk_case_names_induct (List.concat descr');
 
     val (thy9, _) = thy8 |>
       Theory.add_path big_name |>
-      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
+      PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] |>>
       Theory.parent_path |>>>
       DatatypeAux.store_thmss "distinct" new_type_names distinct_thms |>>>
       DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss |>>>
isabelle