1.1 --- a/src/HOL/Nitpick.thy Tue Dec 07 11:56:01 2010 +0100
1.2 +++ b/src/HOL/Nitpick.thy Tue Dec 07 11:56:01 2010 +0100
1.3 @@ -76,6 +76,9 @@
1.4 "tranclp r a b \<equiv> trancl (split r) (a, b)"
1.5 by (simp add: trancl_def Collect_def mem_def)
1.6
1.7 +definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
1.8 +"prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
1.9 +
1.10 definition refl' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.11 "refl' r \<equiv> \<forall>x. (x, x) \<in> r"
1.12
1.13 @@ -237,18 +240,18 @@
1.14 setup {* Nitpick_Isar.setup *}
1.15
1.16 hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
1.17 - FinFun FunBox PairBox Word refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
1.18 - fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
1.19 - one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
1.20 + FinFun FunBox PairBox Word prod refl' wf' wf_wfrec wf_wfrec' wfrec' card'
1.21 + setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac
1.22 + zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
1.23 number_of_frac inverse_frac less_frac less_eq_frac of_frac
1.24 hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
1.25 word
1.26 -hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
1.27 - wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
1.28 - The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
1.29 - nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
1.30 - num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def
1.31 - uminus_frac_def number_of_frac_def inverse_frac_def less_frac_def
1.32 - less_eq_frac_def of_frac_def
1.33 +hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def prod_def
1.34 + refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
1.35 + fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def
1.36 + list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
1.37 + zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
1.38 + plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
1.39 + inverse_frac_def less_frac_def less_eq_frac_def of_frac_def
1.40
1.41 end