(* Title: LK/ex/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"];