src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 64845 e5d4bc2016a6
parent 63950 cdc1e59aa513
child 67091 1393c2340eec