Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nominal/nominal_package.ML
changeset 22543 9460a4cf0acc
parent 22529 902ed60d53a7
child 22578 b0eb5652f210 
--- a/src/HOL/Nominal/nominal_package.ML	Wed Mar 28 19:16:11 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Wed Mar 28 19:17:40 2007 +0200
@@ -1137,8 +1137,8 @@
  
     val (_, thy9) = thy8 |>
       Theory.add_path big_name |>
-      PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] ||>>
-      PureThy.add_thmss [(("inducts_weak", projections dt_induct), [case_names_induct])] ||>
+      PureThy.add_thms [(("weak_induct", dt_induct), [case_names_induct])] ||>>
+      PureThy.add_thmss [(("weak_inducts", projections dt_induct), [case_names_induct])] ||>
       Theory.parent_path ||>>
       DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
       DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
isabelle