theory IMP_1 imports "HOL-Library.Predicate_Compile_Quickcheck" begin subsection ‹IMP› text ‹ In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, and IF. › type_synonym var = unit type_synonym state = bool