# HG changeset patch # User blanchet # Date 1392222959 -3600 # Node ID 3def821deb70ff21ac1cac8662064e03f3a6942d # Parent 17fb554688f0dce45fdbd9f6e69fba3328ae3533 don't hide constant forever, since it may appear in some 'primcorec'-generated theorems diff -r 17fb554688f0 -r 3def821deb70 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Wed Feb 12 17:35:59 2014 +0100 +++ b/src/HOL/Nat.thy Wed Feb 12 17:35:59 2014 +0100 @@ -82,7 +82,7 @@ apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst]) done -wrap_free_constructors ["0 \ nat", Suc] case_nat [=] [[], [pred]] +wrap_free_constructors ["0 \ nat", Suc] case_nat [=] [[], [pred]] [[pred: "0 \ nat"]] apply atomize_elim apply (rename_tac n, induct_tac n rule: nat_induct0, auto) apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI @@ -121,7 +121,7 @@ declare nat.sel[code del] -hide_const Nat.pred -- {* hide everything related to the selector *} +hide_const (open) Nat.pred -- {* hide everything related to the selector *} hide_fact nat.case_eq_if nat.collapse