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.
Renamed induct(s)_weak to weak_induct(s) in order to unify
authorberghofe
Wed, 28 Mar 2007 19:17:40 +0200
changeset 22543 9460a4cf0acc
parent 22542 8279a25ad0ae
child 22544 549615dcd4f2
Renamed induct(s)_weak to weak_induct(s) in order to unify naming scheme with the one used in nominal_inductive.
src/HOL/Nominal/nominal_package.ML file | annotate | diff | comparison | revisions 
--- 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