formal markup of @{syntax_const} and @{const_syntax};
authentic syntax for extra robustness;
(* Title: Sequents/LK/ROOT.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Examples for Classical Logic.
*)
use_thys ["Propositional", "Quantifiers", "Hard_Quantifiers", "Nat"];