src/HOL/Nonstandard_Analysis/StarDef.thy
changeset 68684 9a42b84f8838
parent 67635 28f926146986
child 69064 5840724b1d71
equal deleted inserted replaced
68683:d69127c6e80f 68684:9a42b84f8838