Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
changeset 59275 77cd4992edcd
parent 59058 a78612c67ec0
child 59276 d207455817e8 
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Dec 19 11:20:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Dec 19 14:06:13 2014 +0100
@@ -154,6 +154,8 @@
       BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
       BNF_FP_Util.fp_result * local_theory) ->
     (local_theory -> local_theory) parser
+
+  val mk_parametricity_goal: Proof.context -> term list -> term -> term -> term
 end;
 
 structure BNF_FP_Def_Sugar : BNF_FP_DEF_SUGAR =
isabelle