src/HOL/Code_Setup.thy
changeset 25885 6fbc3f54f819
parent 25866 263aaf988d44
child 25916 d957d9982241
equal deleted inserted replaced
25884:a69e665b7df8 25885:6fbc3f54f819
    18   "bool"  ("bool")
    18   "bool"  ("bool")
    19 attach (term_of) {*
    19 attach (term_of) {*
    20 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    20 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    21 *}
    21 *}
    22 attach (test) {*
    22 attach (test) {*
    23 fun gen_bool i = one_of [false, true];
    23 fun gen_bool i =
       
    24   let val b = one_of [false, true]
       
    25   in (b, fn () => term_of_bool b) end;
    24 *}
    26 *}
    25   "prop"  ("bool")
    27   "prop"  ("bool")
    26 attach (term_of) {*
    28 attach (term_of) {*
    27 fun term_of_prop b =
    29 fun term_of_prop b =
    28   HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
    30   HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);