src/HOL/Matrix/Float.thy
changeset 15537 5538d3244b4d
parent 15236 f289e8ba2bb3
equal deleted inserted replaced
15536:3ce1cb7a24f0 15537:5538d3244b4d