# HG changeset patch
# User blanchet
# Date 1298285438 -3600
# Node ID 0c6093d596d636d078810a2a0602a27bf4a57689
# Parent  afd7405f1d7ec0434d25d7de032e614f70b5e148
rename Nitpick's (internal) auxiliary lemmas

diff -r afd7405f1d7e -r 0c6093d596d6 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Nitpick.thy	Mon Feb 21 11:50:38 2011 +0100
@@ -47,7 +47,7 @@
 Alternative definitions.
 *}
 
-lemma Ex1_def [nitpick_unfold, no_atp]:
+lemma Ex1_unfold [nitpick_unfold, no_atp]:
 "Ex1 P \<equiv> \<exists>x. P = {x}"
 apply (rule eq_reflection)
 apply (simp add: Ex1_def set_eq_iff)
@@ -60,14 +60,14 @@
  apply (erule_tac x = y in allE)
 by (auto simp: mem_def)
 
-lemma rtrancl_def [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
+lemma rtrancl_unfold [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
 by simp
 
-lemma rtranclp_def [nitpick_unfold, no_atp]:
+lemma rtranclp_unfold [nitpick_unfold, no_atp]:
 "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)"
 by (rule eq_reflection) (auto dest: rtranclpD)
 
-lemma tranclp_def [nitpick_unfold, no_atp]:
+lemma tranclp_unfold [nitpick_unfold, no_atp]:
 "tranclp r a b \<equiv> trancl (split r) (a, b)"
 by (simp add: trancl_def Collect_def mem_def)
 
@@ -115,7 +115,7 @@
 apply (erule contrapos_np)
 by (rule someI)
 
-lemma unit_case_def [nitpick_unfold, no_atp]:
+lemma unit_case_unfold [nitpick_unfold, no_atp]:
 "unit_case x u \<equiv> x"
 apply (subgoal_tac "u = ()")
  apply (simp only: unit.cases)
@@ -123,7 +123,7 @@
 
 declare unit.cases [nitpick_simp del]
 
-lemma nat_case_def [nitpick_unfold, no_atp]:
+lemma nat_case_unfold [nitpick_unfold, no_atp]:
 "nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
 apply (rule eq_reflection)
 by (case_tac n) auto
@@ -240,9 +240,9 @@
     one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
     number_of_frac inverse_frac less_frac less_eq_frac of_frac
 hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
-hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def prod_def
-    refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
-    fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def
+hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
+    prod_def refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
+    fold_graph'_def The_psimp Eps_psimp unit_case_unfold nat_case_unfold
     list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
     zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
     plus_frac_def times_frac_def uminus_frac_def number_of_frac_def