export ML function
authorblanchet
Tue Mar 22 07:57:02 2016 +0100 (2016-03-22)
changeset 626866e8924f957f6
parent 62685 1e5cf471e703
child 62687 1c4842b32bfb
export ML function
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 22 07:57:01 2016 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 22 07:57:02 2016 +0100
     1.3 @@ -57,6 +57,7 @@
     1.4    val s_disjs: term list -> term
     1.5    val s_dnf: term list list -> term list
     1.6  
     1.7 +  val case_of: Proof.context -> string -> (string * bool) option
     1.8    val fold_rev_let_if_case: Proof.context -> (term list -> term -> 'a -> 'a) -> typ list ->
     1.9      term -> 'a -> 'a
    1.10    val massage_let_if_case: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->