src/HOL/ex/Predicate_Compile_ex.thy
changeset 32777 8ae3a48c69d9
parent 32673 d5db9cf85401
child 33104 560372b461e5