data61 / PSL

Other
65 stars 9 forks source link

LiFtEr: Pattern and Isabelle keyword to define constants. #86

Closed yutakang closed 3 years ago

yutakang commented 5 years ago

The atomic assertion, Pattern, should tell which Isabelle keyword was used to define the constant at hand.

yutakang commented 3 years ago

LiFtEr got replaced by SeLFiE.