src/HOL/Nitpick.thy
changeset 34982 7b8c366e34a2
parent 34938 f4d3daddac42
child 35028 108662d50512
child 35070 96136eb6218f
     1.1 --- a/src/HOL/Nitpick.thy	Mon Feb 01 14:12:12 2010 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Tue Feb 02 11:38:38 2010 +0100
     1.3 @@ -36,6 +36,7 @@
     1.4             and bisim_iterator_max :: bisim_iterator
     1.5             and Quot :: "'a \<Rightarrow> 'b"
     1.6             and quot_normal :: "'a \<Rightarrow> 'a"
     1.7 +           and NonStd :: "'a \<Rightarrow> 'b"
     1.8             and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
     1.9  
    1.10  datatype ('a, 'b) pair_box = PairBox 'a 'b
    1.11 @@ -43,6 +44,7 @@
    1.12  
    1.13  typedecl unsigned_bit
    1.14  typedecl signed_bit
    1.15 +typedecl \<xi>
    1.16  
    1.17  datatype 'a word = Word "('a set)"
    1.18  
    1.19 @@ -250,12 +252,12 @@
    1.20  setup {* Nitpick_Isar.setup *}
    1.21  
    1.22  hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
    1.23 -    bisim_iterator_max Quot quot_normal Tha PairBox FunBox Word refl' wf'
    1.24 +    bisim_iterator_max Quot quot_normal NonStd Tha PairBox FunBox Word refl' wf'
    1.25      wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd
    1.26      int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac
    1.27      plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac
    1.28      of_frac
    1.29 -hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
    1.30 +hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit \<xi> word
    1.31  hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
    1.32      wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
    1.33      The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def