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