src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
changeset 62686 6e8924f957f6
parent 62583 8c7301325f9f
child 62698 9d706e37ddab
equal deleted inserted replaced
62685:1e5cf471e703 62686:6e8924f957f6
    55   val s_not_conj: term list -> term list
    55   val s_not_conj: term list -> term list
    56   val s_conjs: term list -> term
    56   val s_conjs: term list -> term
    57   val s_disjs: term list -> term
    57   val s_disjs: term list -> term
    58   val s_dnf: term list list -> term list
    58   val s_dnf: term list list -> term list
    59 
    59 
       
    60   val case_of: Proof.context -> string -> (string * bool) option
    60   val fold_rev_let_if_case: Proof.context -> (term list -> term -> 'a -> 'a) -> typ list ->
    61   val fold_rev_let_if_case: Proof.context -> (term list -> term -> 'a -> 'a) -> typ list ->
    61     term -> 'a -> 'a
    62     term -> 'a -> 'a
    62   val massage_let_if_case: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
    63   val massage_let_if_case: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
    63     (typ list -> term -> unit) -> (typ list -> term -> term) -> typ list -> term -> term
    64     (typ list -> term -> unit) -> (typ list -> term -> term) -> typ list -> term -> term
    64   val massage_nested_corec_call: Proof.context -> (term -> bool) ->
    65   val massage_nested_corec_call: Proof.context -> (term -> bool) ->