src/HOL/Tools/inductive_realizer.ML
changeset 59523 860fb1c65553
parent 59498 50b60f501b05
child 59582 0fbed69ff081
equal deleted inserted replaced
59522:0c5c5ad5d2e0 59523:860fb1c65553