src/HOL/ex/predicate_compile.ML
changeset 30705 e8ab35c6ade6
parent 30528 7173bf123335
child 30972 5b65835ccc92
child 31105 95f66b234086
equal deleted inserted replaced
30704:d6d4828e74a2 30705:e8ab35c6ade6