src/HOL/Tools/inductive.ML
changeset 79983 ee45e96eb7c5
parent 79732 a53287d9add3
child 80636 4041e7c8059d
equal deleted inserted replaced
79973:7bbb0d65ce72 79983:ee45e96eb7c5