src/HOL/Tools/BNF/bnf_comp.ML
changeset 67917 d13b2dd20f5e
parent 67091 1393c2340eec
child 68960 b85d509e7cbf
equal deleted inserted replaced
67916:a72f01c63262 67917:d13b2dd20f5e