src/HOL/Inductive.thy
changeset 29457 2eadbc24de8c
parent 29281 b22ccb3998db
child 31604 eb2f9d709296
equal deleted inserted replaced
29456:3f8b85444512 29457:2eadbc24de8c