src/HOL/Nitpick.thy
changeset 41797 0c6093d596d6
parent 41792 ff3cb0c418b7
child 42064 f4e53c8630c0
     1.1 --- a/src/HOL/Nitpick.thy	Mon Feb 21 11:50:38 2011 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Mon Feb 21 11:50:38 2011 +0100
     1.3 @@ -47,7 +47,7 @@
     1.4  Alternative definitions.
     1.5  *}
     1.6  
     1.7 -lemma Ex1_def [nitpick_unfold, no_atp]:
     1.8 +lemma Ex1_unfold [nitpick_unfold, no_atp]:
     1.9  "Ex1 P \<equiv> \<exists>x. P = {x}"
    1.10  apply (rule eq_reflection)
    1.11  apply (simp add: Ex1_def set_eq_iff)
    1.12 @@ -60,14 +60,14 @@
    1.13   apply (erule_tac x = y in allE)
    1.14  by (auto simp: mem_def)
    1.15  
    1.16 -lemma rtrancl_def [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
    1.17 +lemma rtrancl_unfold [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
    1.18  by simp
    1.19  
    1.20 -lemma rtranclp_def [nitpick_unfold, no_atp]:
    1.21 +lemma rtranclp_unfold [nitpick_unfold, no_atp]:
    1.22  "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)"
    1.23  by (rule eq_reflection) (auto dest: rtranclpD)
    1.24  
    1.25 -lemma tranclp_def [nitpick_unfold, no_atp]:
    1.26 +lemma tranclp_unfold [nitpick_unfold, no_atp]:
    1.27  "tranclp r a b \<equiv> trancl (split r) (a, b)"
    1.28  by (simp add: trancl_def Collect_def mem_def)
    1.29  
    1.30 @@ -115,7 +115,7 @@
    1.31  apply (erule contrapos_np)
    1.32  by (rule someI)
    1.33  
    1.34 -lemma unit_case_def [nitpick_unfold, no_atp]:
    1.35 +lemma unit_case_unfold [nitpick_unfold, no_atp]:
    1.36  "unit_case x u \<equiv> x"
    1.37  apply (subgoal_tac "u = ()")
    1.38   apply (simp only: unit.cases)
    1.39 @@ -123,7 +123,7 @@
    1.40  
    1.41  declare unit.cases [nitpick_simp del]
    1.42  
    1.43 -lemma nat_case_def [nitpick_unfold, no_atp]:
    1.44 +lemma nat_case_unfold [nitpick_unfold, no_atp]:
    1.45  "nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
    1.46  apply (rule eq_reflection)
    1.47  by (case_tac n) auto
    1.48 @@ -240,9 +240,9 @@
    1.49      one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
    1.50      number_of_frac inverse_frac less_frac less_eq_frac of_frac
    1.51  hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
    1.52 -hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def prod_def
    1.53 -    refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
    1.54 -    fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def
    1.55 +hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
    1.56 +    prod_def refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
    1.57 +    fold_graph'_def The_psimp Eps_psimp unit_case_unfold nat_case_unfold
    1.58      list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
    1.59      zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
    1.60      plus_frac_def times_frac_def uminus_frac_def number_of_frac_def