src/HOL/cladata.ML
changeset 20145 922b4e7b8efd
parent 18708 4b3dadb4fe33
child 20223 89d2758ecddf
equal deleted inserted replaced
20144:2517cd4b1f37 20145:922b4e7b8efd