src/Pure/ML/ml_context.ML
changeset 24581 6491d89ba76c
parent 24574 e840872e9c7c
child 24685 c3d56f41483b
equal deleted inserted replaced
24580:916259859344 24581:6491d89ba76c
     1 (*  Title:      Pure/Thy/ml_context.ML
     1 (*  Title:      Pure/ML/ml_context.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Makarius
     3     Author:     Makarius
     4 
     4 
     5 ML context and antiquotations.
     5 ML context and antiquotations.
     6 *)
     6 *)