src/HOL/Quickcheck_Examples/Completeness.thy
changeset 58813 625d04d4fd2a
parent 57645 ee55e667dedc
child 58889 5b7a9633cfa8
equal deleted inserted replaced
58812:5a9a2d3b9f8b 58813:625d04d4fd2a
    18 
    18 
    19 lemma is_some_is_not_None:
    19 lemma is_some_is_not_None:
    20   "is_some x \<longleftrightarrow> x \<noteq> None"
    20   "is_some x \<longleftrightarrow> x \<noteq> None"
    21   by (cases x) simp_all
    21   by (cases x) simp_all
    22 
    22 
    23 setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *} 
    23 setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
    24 
    24 
    25 subsection {* Defining the size of values *}
    25 subsection {* Defining the size of values *}
    26 
    26 
    27 hide_const size
    27 hide_const size
    28 
    28