CODEWITHSUNDEEP
isabellehol
W_zw
W_zw

Reputation: 1

How to write expansion rules in Isabelle？

I encountered some problems while learning Isabelle's expansion rules. I hope someone can answer them, thank you.

  1. I need to import Isabella's built-in HOL library to introduce some defined quantifiers. When I use Isabella2017 to open %ISABELLE_HOME%\src\HOL\HOL.thy, the seventh line "theory HOL" will report an error "Cannot update finished theory"HOL.HOL" ".

  2. Have you encountered the same problem? How did you introduce the built-in rules in the HOL library?

Upvotes: 0

Views: 66

Answers (0)

Related Questions