doc-src/TutorialI/Rules/ROOT.ML

back to plain Position.report for regular references;
ContextPosition.report_visible for decls;
report_token/parse_token: back to context-less version;

(* ID:         $Id$ *)
use_thy "Basic";
use_thy "Blast";
use_thy "Force";
use_thy "Forward";
use_thy "Tacticals";

use_thy "find2";