src/HOL/Tools/enriched_type.ML
changeset 41792 ff3cb0c418b7
parent 41505 6d19301074cf
child 42361 23f352990944
equal deleted inserted replaced
41791:01d722707a36 41792:ff3cb0c418b7