Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
export more functions
authorblanchet
Thu, 26 Mar 2015 16:42:42 +0100
changeset 59818 41f0804b7309
parent 59817 75433c3ee203
child 59819 dbec7f33093d
export more functions
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Mar 26 12:00:32 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Mar 26 16:42:42 2015 +0100
@@ -83,6 +83,8 @@
 
   val flat_corec_preds_predsss_gettersss: 'a list -> 'a list list list -> 'a list list list ->
     'a list
+  val mk_ctor: typ list -> term -> term
+  val mk_dtor: typ list -> term -> term
   val liveness_of_fp_bnf: int -> BNF_Def.bnf -> bool list
   val nesting_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
isabelle