# HG changeset patch # User wenzelm # Date 1429189864 -7200 # Node ID 7b98dbc1d13efe75e9c9ce8fd3c76f0ecc4f6849 # Parent 35f626b1142229f7df674a1007ce26d26889ad7e tuned comment; diff -r 35f626b11422 -r 7b98dbc1d13e src/Pure/pure_syn.ML --- a/src/Pure/pure_syn.ML Thu Apr 16 15:00:03 2015 +0200 +++ b/src/Pure/pure_syn.ML Thu Apr 16 15:11:04 2015 +0200 @@ -1,7 +1,8 @@ (* Title: Pure/pure_syn.ML Author: Makarius -Outer syntax for bootstrapping Isabelle/Pure. +Outer syntax for bootstrapping: commands that are accessible outside a +regular theory context. *) signature PURE_SYN =