equal
deleted
inserted
replaced
8 infix aconvc; |
8 infix aconvc; |
9 |
9 |
10 signature THM = |
10 signature THM = |
11 sig |
11 sig |
12 include THM |
12 include THM |
13 val aconvc : cterm * cterm -> bool |
13 val aconvc: cterm * cterm -> bool |
14 val add_cterm_frees: cterm -> cterm list -> cterm list |
14 val add_cterm_frees: cterm -> cterm list -> cterm list |
15 val mk_binop: cterm -> cterm -> cterm -> cterm |
15 val mk_binop: cterm -> cterm -> cterm -> cterm |
16 val dest_binop: cterm -> cterm * cterm |
16 val dest_binop: cterm -> cterm * cterm |
17 val dest_implies: cterm -> cterm * cterm |
17 val dest_implies: cterm -> cterm * cterm |
18 val dest_equals: cterm -> cterm * cterm |
18 val dest_equals: cterm -> cterm * cterm |