src/HOL/Inductive.ML
changeset 3225 cee363fc07d7
parent 2855 36f75c4a0047
child 3768 67f4ac759100
equal deleted inserted replaced
3224:4ea2aa9f93a5 3225:cee363fc07d7