I'm looking at the 'Haskell-style type classes with Isabelle/Isar' tutorial available online in the Isabelle website, and I've found the that symmetric property in page 2 is stated as:

*sym: eq x y <--> eq x y*

Not sure if I am missing something here, but I assume it should be *eq x y <--> eq y x*.

Last updated: Oct 12 2024 at 20:18 UTC