don't hide constant forever, since it may appear in some 'primcorec'-generated theorems
authorblanchet
Wed Feb 12 17:35:59 2014 +0100 (2014-02-12)
changeset 554433def821deb70
parent 55442 17fb554688f0
child 55444 ec73f81e49e7
don't hide constant forever, since it may appear in some 'primcorec'-generated theorems
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Wed Feb 12 17:35:59 2014 +0100
     1.2 +++ b/src/HOL/Nat.thy	Wed Feb 12 17:35:59 2014 +0100
     1.3 @@ -82,7 +82,7 @@
     1.4  apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
     1.5  done
     1.6  
     1.7 -wrap_free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]]
     1.8 +wrap_free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]] [[pred: "0 \<Colon> nat"]]
     1.9    apply atomize_elim
    1.10    apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
    1.11   apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI
    1.12 @@ -121,7 +121,7 @@
    1.13  
    1.14  declare nat.sel[code del]
    1.15  
    1.16 -hide_const Nat.pred -- {* hide everything related to the selector *}
    1.17 +hide_const (open) Nat.pred -- {* hide everything related to the selector *}
    1.18  hide_fact
    1.19    nat.case_eq_if
    1.20    nat.collapse