src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
changeset 41171 043f8dc3b51f
parent 40052 ea46574ca815
child 41225 bd4ecd48c21f