src/HOL/Main.thy
changeset 15395 b93cdbac8f46
parent 15382 e56ce5cefe9c
child 15531 08c8dad8e399
     1.1 --- a/src/HOL/Main.thy	Fri Dec 10 16:48:01 2004 +0100
     1.2 +++ b/src/HOL/Main.thy	Fri Dec 10 16:48:29 2004 +0100
     1.3 @@ -19,7 +19,6 @@
     1.4  
     1.5  types_code
     1.6    "bool"  ("bool")
     1.7 -  "*"     ("(_ */ _)")
     1.8  
     1.9  consts_code
    1.10    "True"    ("true")
    1.11 @@ -29,10 +28,6 @@
    1.12    "op &"    ("(_ andalso/ _)")
    1.13    "If"      ("(if _/ then _/ else _)")
    1.14  
    1.15 -  "Pair"    ("(_,/ _)")
    1.16 -  "fst"     ("fst")
    1.17 -  "snd"     ("snd")
    1.18 -
    1.19    "wfrec"   ("wf'_rec?")
    1.20  
    1.21  quickcheck_params [default_type = int]
    1.22 @@ -42,7 +37,6 @@
    1.23  
    1.24  fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    1.25  val term_of_int = HOLogic.mk_int;
    1.26 -fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
    1.27  fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
    1.28  
    1.29  val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"
    1.30 @@ -65,8 +59,6 @@
    1.31  
    1.32  fun gen_int i = one_of [~1, 1] * random_range 0 i;
    1.33  
    1.34 -fun gen_id_42 aG bG i = (aG i, bG i);
    1.35 -
    1.36  fun gen_fun_type _ G i =
    1.37    let
    1.38      val f = ref (fn x => raise ERROR);