src/HOL/Tools/Predicate_Compile/mode_inference.ML
changeset 81920 8d5989ab1e42
parent 80636 4041e7c8059d
equal deleted inserted replaced
81919:f4cd3e679096 81920:8d5989ab1e42