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.
called the induction principle "unsafe" instead of "test".
authorurbanc
Thu, 10 Nov 2005 00:36:26 +0100
changeset 18142 a51ab4152097
parent 18141 89e2e8bed08f
child 18143 fe14f0282c60
called the induction principle "unsafe" instead of "test".
src/HOL/Nominal/nominal_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nominal/nominal_package.ML	Wed Nov 09 18:01:33 2005 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Thu Nov 10 00:36:26 2005 +0100
@@ -1088,7 +1088,7 @@
             (AxClass.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
         end) (atoms ~~ finite_supp_thms) |>>
       Theory.add_path big_name |>>>
-      PureThy.add_axioms_i [(("induct_test", induct), [case_names_induct])] |>>
+      PureThy.add_axioms_i [(("induct_unsafe", induct), [case_names_induct])] |>>
       Theory.parent_path;
 
   in
isabelle