src/HOL/Main.thy
changeset 16770 1f1b1fae30e4
parent 16635 bf7de5723c60
child 17386 b110730a24fd
     1.1 --- a/src/HOL/Main.thy	Tue Jul 12 11:41:24 2005 +0200
     1.2 +++ b/src/HOL/Main.thy	Tue Jul 12 11:51:31 2005 +0200
     1.3 @@ -19,6 +19,12 @@
     1.4  
     1.5  types_code
     1.6    "bool"  ("bool")
     1.7 +attach (term_of) {*
     1.8 +fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
     1.9 +*}
    1.10 +attach (test) {*
    1.11 +fun gen_bool i = one_of [false, true];
    1.12 +*}
    1.13  
    1.14  consts_code
    1.15    "True"    ("true")
    1.16 @@ -28,18 +34,14 @@
    1.17    "op &"    ("(_ andalso/ _)")
    1.18    "HOL.If"      ("(if _/ then _/ else _)")
    1.19  
    1.20 -  "wfrec"   ("wf'_rec?")
    1.21 +  "wfrec"   ("\<module>wf'_rec?")
    1.22 +attach {*
    1.23 +fun wf_rec f x = f (wf_rec f) x;
    1.24 +*}
    1.25  
    1.26  quickcheck_params [default_type = int]
    1.27  
    1.28 -(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
    1.29  ML {*
    1.30 -fun wf_rec f x = f (wf_rec f) x;
    1.31 -
    1.32 -fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    1.33 -val term_of_int = HOLogic.mk_int o IntInf.fromInt;
    1.34 -fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
    1.35 -
    1.36  local
    1.37  
    1.38  fun eq_codegen thy defs gr dep thyname b t =
    1.39 @@ -62,20 +64,6 @@
    1.40  val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];
    1.41  
    1.42  end;
    1.43 -
    1.44 -fun gen_bool i = one_of [false, true];
    1.45 -
    1.46 -fun gen_int i = one_of [~1, 1] * random_range 0 i;
    1.47 -
    1.48 -fun gen_fun_type _ G i =
    1.49 -  let
    1.50 -    val f = ref (fn x => raise ERROR);
    1.51 -    val _ = (f := (fn x =>
    1.52 -      let
    1.53 -        val y = G i;
    1.54 -        val f' = !f
    1.55 -      in (f := (fn x' => if x = x' then y else f' x'); y) end))
    1.56 -  in (fn x => !f x) end;
    1.57  *}
    1.58  
    1.59  setup eq_codegen_setup