tuned header;
authorwenzelm
Mon, 29 Feb 2016 22:32:04 +0100
changeset 62478 a62c86d25024
parent 62477 bc6e771e98a6
child 62479 716336f19aa9
tuned header;
src/Pure/RAW/ml_heap_polyml-5.3.0.ML
--- a/src/Pure/RAW/ml_heap_polyml-5.3.0.ML	Mon Feb 29 21:32:53 2016 +0100
+++ b/src/Pure/RAW/ml_heap_polyml-5.3.0.ML	Mon Feb 29 22:32:04 2016 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Pure/RAW/ml_heap.ML
+(*  Title:      Pure/RAW/ml_heap_polyml-5.3.0.ML
     Author:     Makarius
 
 ML heap operations.