src/HOL/Inductive.thy
changeset 18396 b3e7da94b51f
parent 17009 932e0e370926
child 18456 8cc35e95450a
equal deleted inserted replaced
18395:87217764cec2 18396:b3e7da94b51f