equal
deleted
inserted
replaced
134 val dest_imp = dest_binop "op -->" |
134 val dest_imp = dest_binop "op -->" |
135 val dest_conj = dest_binop "op &" |
135 val dest_conj = dest_binop "op &" |
136 val dest_disj = dest_binop "op |" |
136 val dest_disj = dest_binop "op |" |
137 val dest_cons = dest_binop "Cons" |
137 val dest_cons = dest_binop "Cons" |
138 val dest_let = Library.swap o dest_binop "Let"; |
138 val dest_let = Library.swap o dest_binop "Let"; |
139 val dest_select = dest_binder "Eps" |
139 val dest_select = dest_binder "Hilbert_Choice.Eps" |
140 val dest_exists = dest_binder "Ex" |
140 val dest_exists = dest_binder "Ex" |
141 val dest_forall = dest_binder "All" |
141 val dest_forall = dest_binder "All" |
142 |
142 |
143 (* Query routines *) |
143 (* Query routines *) |
144 |
144 |