src/HOL/datatype.ML
changeset 4176 84a0bfbd74e5
parent 4107 2270829d2364
child 4184 23a09f2fd687
equal deleted inserted replaced
4175:06774cd43054 4176:84a0bfbd74e5