src/HOL/Library/Tree_Real.thy
changeset 68593 d32d40d03e0a
parent 68484 59793df7f853
child 68998 818898556504
equal deleted inserted replaced
68589:9258f16d68b4 68593:d32d40d03e0a