called the induction principle "unsafe" instead of "test".
authorurbanc
Thu Nov 10 00:36:26 2005 +0100 (2005-11-10)
changeset 18142a51ab4152097
parent 18141 89e2e8bed08f
child 18143 fe14f0282c60
called the induction principle "unsafe" instead of "test".
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Nov 09 18:01:33 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Thu Nov 10 00:36:26 2005 +0100
     1.3 @@ -1088,7 +1088,7 @@
     1.4              (AxClass.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
     1.5          end) (atoms ~~ finite_supp_thms) |>>
     1.6        Theory.add_path big_name |>>>
     1.7 -      PureThy.add_axioms_i [(("induct_test", induct), [case_names_induct])] |>>
     1.8 +      PureThy.add_axioms_i [(("induct_unsafe", induct), [case_names_induct])] |>>
     1.9        Theory.parent_path;
    1.10  
    1.11    in