src/CTT/ex/ROOT.ML

-(*  Title:      CTT/ex/ROOT.ML
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-
-Examples for Constructive Type Theory. 
-*)
-
-use_thys ["Typechecking", "Elimination", "Equality", "Synthesis"];