equal
deleted
inserted
replaced
125 handle U.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected); |
125 handle U.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected); |
126 |
126 |
127 |
127 |
128 val dest_neg = dest_monop @{const_name Not} |
128 val dest_neg = dest_monop @{const_name Not} |
129 val dest_pair = dest_binop @{const_name Pair} |
129 val dest_pair = dest_binop @{const_name Pair} |
130 val dest_eq = dest_binop @{const_name "op ="} |
130 val dest_eq = dest_binop @{const_name HOL.eq} |
131 val dest_imp = dest_binop @{const_name HOL.implies} |
131 val dest_imp = dest_binop @{const_name HOL.implies} |
132 val dest_conj = dest_binop @{const_name HOL.conj} |
132 val dest_conj = dest_binop @{const_name HOL.conj} |
133 val dest_disj = dest_binop @{const_name HOL.disj} |
133 val dest_disj = dest_binop @{const_name HOL.disj} |
134 val dest_select = dest_binder @{const_name Eps} |
134 val dest_select = dest_binder @{const_name Eps} |
135 val dest_exists = dest_binder @{const_name Ex} |
135 val dest_exists = dest_binder @{const_name Ex} |