src/HOL/Nitpick.thy
changeset 35177 168041f24f80
parent 35079 592edca1dfb3
child 35180 c57dba973391
     1.1 --- a/src/HOL/Nitpick.thy	Wed Feb 10 11:47:33 2010 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Fri Feb 12 19:44:37 2010 +0100
     1.3 @@ -37,7 +37,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 Silly :: "'a \<Rightarrow> 'b"
     1.9             and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
    1.10  
    1.11  datatype ('a, 'b) pair_box = PairBox 'a 'b
    1.12 @@ -254,7 +254,7 @@
    1.13  setup {* Nitpick_Isar.setup *}
    1.14  
    1.15  hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
    1.16 -    bisim_iterator_max Quot quot_normal NonStd Tha PairBox FunBox Word refl' wf'
    1.17 +    bisim_iterator_max Quot quot_normal Silly Tha PairBox FunBox Word refl' wf'
    1.18      wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd
    1.19      int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac
    1.20      plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac