search

data61 / PSL

Other
65 stars 9 forks source link

SeLFiE: use utility functions in Pure/logic.ML to implement Unique_Node #175

Closed yutakang closed 4 years ago

yutakang commented 4 years ago

For example, we can handle the deconstruction/flattening of nested implications using Logic.strip_imp_prems.

yutakang commented 4 years ago

We can also use Logic.dest_conjunctions for &&&.

yutakang commented 4 years ago

No... we cannot use these functions there. utrm_w_prnt_to_futrm_w_prnt takes utrm_w_prnt not term.