src/HOL/HOL.thy
changeset 45171 262f179665f9
parent 45133 2214ba5bdfff
child 45231 d85a2fdc586c
     1.1 --- a/src/HOL/HOL.thy	Wed Oct 19 08:37:15 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Oct 19 08:37:16 2011 +0200
     1.3 @@ -28,7 +28,6 @@
     1.4    "~~/src/Tools/induct.ML"
     1.5    ("~~/src/Tools/induction.ML")
     1.6    ("~~/src/Tools/induct_tacs.ML")
     1.7 -  ("Tools/recfun_codegen.ML")
     1.8    ("Tools/cnf_funcs.ML")
     1.9    "~~/src/Tools/subtyping.ML"
    1.10    "~~/src/Tools/case_product.ML"
    1.11 @@ -1715,66 +1714,6 @@
    1.12  
    1.13  subsection {* Code generator setup *}
    1.14  
    1.15 -subsubsection {* SML code generator setup *}
    1.16 -
    1.17 -use "Tools/recfun_codegen.ML"
    1.18 -
    1.19 -setup {*
    1.20 -  Codegen.setup
    1.21 -  #> RecfunCodegen.setup
    1.22 -  #> Codegen.map_unfold (K HOL_basic_ss)
    1.23 -*}
    1.24 -
    1.25 -types_code
    1.26 -  "bool"  ("bool")
    1.27 -attach (term_of) {*
    1.28 -fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    1.29 -*}
    1.30 -attach (test) {*
    1.31 -fun gen_bool i =
    1.32 -  let val b = one_of [false, true]
    1.33 -  in (b, fn () => term_of_bool b) end;
    1.34 -*}
    1.35 -  "prop"  ("bool")
    1.36 -attach (term_of) {*
    1.37 -fun term_of_prop b =
    1.38 -  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
    1.39 -*}
    1.40 -
    1.41 -consts_code
    1.42 -  "Trueprop" ("(_)")
    1.43 -  "True"    ("true")
    1.44 -  "False"   ("false")
    1.45 -  "Not"     ("Bool.not")
    1.46 -  HOL.disj    ("(_ orelse/ _)")
    1.47 -  HOL.conj    ("(_ andalso/ _)")
    1.48 -  "If"      ("(if _/ then _/ else _)")
    1.49 -
    1.50 -setup {*
    1.51 -let
    1.52 -
    1.53 -fun eq_codegen thy mode defs dep thyname b t gr =
    1.54 -    (case strip_comb t of
    1.55 -       (Const (@{const_name HOL.eq}, Type (_, [Type ("fun", _), _])), _) => NONE
    1.56 -     | (Const (@{const_name HOL.eq}, _), [t, u]) =>
    1.57 -          let
    1.58 -            val (pt, gr') = Codegen.invoke_codegen thy mode defs dep thyname false t gr;
    1.59 -            val (pu, gr'') = Codegen.invoke_codegen thy mode defs dep thyname false u gr';
    1.60 -            val (_, gr''') =
    1.61 -              Codegen.invoke_tycodegen thy mode defs dep thyname false HOLogic.boolT gr'';
    1.62 -          in
    1.63 -            SOME (Codegen.parens
    1.64 -              (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
    1.65 -          end
    1.66 -     | (t as Const (@{const_name HOL.eq}, _), ts) => SOME (Codegen.invoke_codegen
    1.67 -         thy mode defs dep thyname b (Codegen.eta_expand t ts 2) gr)
    1.68 -     | _ => NONE);
    1.69 -
    1.70 -in
    1.71 -  Codegen.add_codegen "eq_codegen" eq_codegen
    1.72 -end
    1.73 -*}
    1.74 -
    1.75  subsubsection {* Generic code generator preprocessor setup *}
    1.76  
    1.77  setup {*
    1.78 @@ -1979,10 +1918,6 @@
    1.79    Scan.succeed (gen_eval_method (Code_Runtime.dynamic_holds_conv o Proof_Context.theory_of))
    1.80  *} "solve goal by evaluation"
    1.81  
    1.82 -method_setup evaluation = {*
    1.83 -  Scan.succeed (gen_eval_method Codegen.evaluation_conv)
    1.84 -*} "solve goal by evaluation"
    1.85 -
    1.86  method_setup normalization = {*
    1.87    Scan.succeed (fn ctxt => SIMPLE_METHOD'
    1.88      (CHANGED_PROP o (CONVERSION (Nbe.dynamic_conv (Proof_Context.theory_of ctxt))