SeLFiE: reorganise the numerous assertions I developed.

data61 / PSL

Other

65 stars 9 forks source link

Closed yutakang closed 3 years ago

yutakang commented 3 years ago

[x] split SeLFiE_Assertion.ML into 3 files: one for Test_Heuristic, one for Induction_Heuristic, and one for Generalization_Heuristic. Be careful about the dependency among assertions.
[x] encapsulate implementation details using signature.
[x] update SeLFiE.thy.

yutakang commented 3 years ago

Maybe we should have a separate file for utility assertions such as node_defined_recursively?