src/HOL/Main.thy
changeset 16635 bf7de5723c60
parent 16587 b34c8aa657a5
child 16770 1f1b1fae30e4
     1.1 --- a/src/HOL/Main.thy	Fri Jul 01 13:54:57 2005 +0200
     1.2 +++ b/src/HOL/Main.thy	Fri Jul 01 13:56:34 2005 +0200
     1.3 @@ -40,21 +40,28 @@
     1.4  val term_of_int = HOLogic.mk_int o IntInf.fromInt;
     1.5  fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
     1.6  
     1.7 -val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"
     1.8 -  (fn thy => fn gr => fn dep => fn b => fn t =>
     1.9 +local
    1.10 +
    1.11 +fun eq_codegen thy defs gr dep thyname b t =
    1.12      (case strip_comb t of
    1.13         (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
    1.14       | (Const ("op =", _), [t, u]) =>
    1.15            let
    1.16 -            val (gr', pt) = Codegen.invoke_codegen thy dep false (gr, t);
    1.17 -            val (gr'', pu) = Codegen.invoke_codegen thy dep false (gr', u)
    1.18 +            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
    1.19 +            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u)
    1.20            in
    1.21              SOME (gr'', Codegen.parens
    1.22                (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
    1.23            end
    1.24       | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
    1.25 -         thy dep b (gr, Codegen.eta_expand t ts 2))
    1.26 -     | _ => NONE))];
    1.27 +         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
    1.28 +     | _ => NONE);
    1.29 +
    1.30 +in
    1.31 +
    1.32 +val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];
    1.33 +
    1.34 +end;
    1.35  
    1.36  fun gen_bool i = one_of [false, true];
    1.37  
    1.38 @@ -73,9 +80,7 @@
    1.39  
    1.40  setup eq_codegen_setup
    1.41  
    1.42 -lemma [code]: "((n::nat) < 0) = False" by simp
    1.43 -lemma [code]: "(0 < Suc n) = True" by simp
    1.44 -lemmas [code] = Suc_less_eq imp_conv_disj
    1.45 +lemmas [code] = imp_conv_disj
    1.46  
    1.47  subsection {* Configuration of the 'refute' command *}
    1.48