src/HOL/Tools/inductive_realizer.ML
changeset 46491 c505ea79e2db
parent 46219 426ed18eba43
child 46708 b138dee7bed3
equal deleted inserted replaced
46490:e4863ab5e09b 46491:c505ea79e2db