src/HOL/Tools/inductive_realizer.ML
changeset 55807 fd31d0e70eb8
parent 55235 4b4627f5912b
child 55954 a29aefc88c8d
equal deleted inserted replaced
55805:f4e9517657b1 55807:fd31d0e70eb8