equal
deleted
inserted
replaced
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) -> |