src/HOL/Nitpick.thy
changeset 61121 efe8b18306b7
parent 61076 bdc1e2f0a86a
child 61681 ca53150406c9
equal deleted inserted replaced
61120:65082457c117 61121:efe8b18306b7
   237 
   237 
   238 hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
   238 hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
   239 
   239 
   240 hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold prod_def refl'_def wf'_def
   240 hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold prod_def refl'_def wf'_def
   241   card'_def setsum'_def fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
   241   card'_def setsum'_def fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
   242   size_list_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
   242   size_list_simp nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
   243   num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def uminus_frac_def
   243   num_def denom_def frac_def plus_frac_def times_frac_def uminus_frac_def
   244   number_of_frac_def inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def
   244   number_of_frac_def inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def
   245   wfrec'_def
   245   wfrec'_def
   246 
   246 
   247 end
   247 end