--- a/src/HOL/BNF/Tools/bnf_def.ML Wed Nov 27 11:08:55 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def.ML Wed Nov 27 15:08:18 2013 +0100
@@ -101,6 +101,15 @@
Proof.context
val print_bnfs: Proof.context -> unit
+ val prepare_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
+ (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) -> typ list option ->
+ binding -> binding -> binding list ->
+ (((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context ->
+ string * term list *
+ ((thm list -> {context: Proof.context, prems: thm list} -> tactic) option * term list list) *
+ ((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) *
+ local_theory * thm list
+
val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
({prems: thm list, context: Proof.context} -> tactic) list ->
({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding ->