changeset 59276 | d207455817e8 |
parent 59275 | 77cd4992edcd |
child 59514 | 509caf5edfa6 |
--- a/src/HOL/Transfer.thy Fri Dec 19 14:06:13 2014 +0100 +++ b/src/HOL/Transfer.thy Mon Jan 05 06:56:15 2015 +0100 @@ -371,12 +371,6 @@ ML_file "Tools/Transfer/transfer_bnf.ML" ML_file "Tools/BNF/bnf_fp_rec_sugar_transfer.ML" -ML {* -val _ = Theory.setup (BNF_LFP_Rec_Sugar.primrec_interpretation - BNF_FP_Rec_Sugar_Transfer.primrec_transfer_pluginN - BNF_FP_Rec_Sugar_Transfer.primrec_transfer_interpretation) -*} - declare pred_fun_def [simp] declare rel_fun_eq [relator_eq]