src/HOL/Quickcheck_Exhaustive.thy
changeset 61121 efe8b18306b7
parent 60758 d8d85a8172b5
child 62364 9209770bdcdf
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Sun Sep 06 19:09:20 2015 +0200
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Sun Sep 06 21:55:13 2015 +0200
     1.3 @@ -646,11 +646,6 @@
     1.4  hide_fact (open) orelse_def
     1.5  no_notation orelse (infixr "orelse" 55)
     1.6  
     1.7 -hide_fact
     1.8 -  exhaustive_int'_def
     1.9 -  exhaustive_integer'_def
    1.10 -  exhaustive_natural'_def
    1.11 -
    1.12  hide_const valtermify_absdummy valtermify_fun_upd valterm_emptyset valtermify_insert valtermify_pair
    1.13    valtermify_Inl valtermify_Inr
    1.14    termify_fun_upd term_emptyset termify_insert termify_pair setify