src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
changeset 81920 8d5989ab1e42
parent 80634 a90ab1ea6458
child 82695 d93ead9ac6df
equal deleted inserted replaced
81919:f4cd3e679096 81920:8d5989ab1e42