src/HOL/Nitpick.thy
changeset 34938 f4d3daddac42
parent 34124 c4628a1dcf75
child 34982 7b8c366e34a2
     1.1 --- a/src/HOL/Nitpick.thy	Wed Jan 20 10:38:19 2010 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Wed Jan 20 11:54:19 2010 +0100
     1.3 @@ -29,10 +29,13 @@
     1.4  typedecl bisim_iterator
     1.5  
     1.6  axiomatization unknown :: 'a
     1.7 +           and is_unknown :: "'a \<Rightarrow> bool"
     1.8             and undefined_fast_The :: 'a
     1.9             and undefined_fast_Eps :: 'a
    1.10             and bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.11             and bisim_iterator_max :: bisim_iterator
    1.12 +           and Quot :: "'a \<Rightarrow> 'b"
    1.13 +           and quot_normal :: "'a \<Rightarrow> 'a"
    1.14             and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
    1.15  
    1.16  datatype ('a, 'b) pair_box = PairBox 'a 'b
    1.17 @@ -246,11 +249,12 @@
    1.18  
    1.19  setup {* Nitpick_Isar.setup *}
    1.20  
    1.21 -hide (open) const unknown undefined_fast_The undefined_fast_Eps bisim 
    1.22 -    bisim_iterator_max Tha PairBox FunBox Word refl' wf' wf_wfrec wf_wfrec'
    1.23 -    wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac
    1.24 -    Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac
    1.25 -    times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac
    1.26 +hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
    1.27 +    bisim_iterator_max Quot quot_normal Tha PairBox FunBox Word refl' wf'
    1.28 +    wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd
    1.29 +    int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac
    1.30 +    plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac
    1.31 +    of_frac
    1.32  hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
    1.33  hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
    1.34      wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def