src/HOL/Tools/inductive_realizer.ML
changeset 28939 08004ce1b167
parent 28814 463c9e9111ae
child 28965 1de908189869
equal deleted inserted replaced
28927:7e631979922f 28939:08004ce1b167