src/HOL/Quickcheck_Narrowing.thy
changeset 46308 e5abbec2697a
parent 46032 0da934e135b0
child 46589 689311986778
equal deleted inserted replaced
46307:ec8f975c059b 46308:e5abbec2697a
   365       x = narrowing_dummy_narrowing :: code_int => bool cons;
   365       x = narrowing_dummy_narrowing :: code_int => bool cons;
   366       y = narrowing_dummy_partial_term_of :: bool itself => narrowing_term => term;
   366       y = narrowing_dummy_partial_term_of :: bool itself => narrowing_term => term;
   367       z = (conv :: _ => _ => unit)  in f)"
   367       z = (conv :: _ => _ => unit)  in f)"
   368 unfolding Let_def ensure_testable_def ..
   368 unfolding Let_def ensure_testable_def ..
   369 
   369 
       
   370 subsection {* Narrowing for sets *}
       
   371 
       
   372 instantiation set :: (narrowing) narrowing
       
   373 begin
       
   374 
       
   375 definition "narrowing_set = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons set) narrowing"
       
   376 
       
   377 instance ..
       
   378 
       
   379 end
   370   
   380   
   371 subsection {* Narrowing for integers *}
   381 subsection {* Narrowing for integers *}
   372 
   382 
   373 
   383 
   374 definition drawn_from :: "'a list => 'a cons"
   384 definition drawn_from :: "'a list => 'a cons"