Stream: General

Topic: Primitive constant specification

view this post on Zulip Gergely Buday (Nov 18 2024 at 09:11):

Do I understand correctly that the primitive constant specification mechanism of higher order logic, described in the 16.5.2 section of Gordon and Melham's Introduction to HOL, is implemented in Isabelle/HOL in

src/HOL/Tools/choice_specification.ML ?

Last updated: Dec 21 2024 at 12:33 UTC