author | blanchet |
Wed, 02 Jun 2010 15:18:48 +0200 | |
changeset 37321 | 9d7cfae95b30 |
parent 37134 | 29bd6c2ffba8 |
child 40239 | c4336e45f199 |
permissions | -rw-r--r-- |
(* Title: FOL/ex/ROOT.ML Examples for First-Order Logic. *) use_thys [ "First_Order_Logic", "Natural_Numbers", "Intro", "Nat", "Nat_Class", "Foundation", "Prolog", "Intuitionistic", "Propositional_Int", "Quantifiers_Int", "Classical", "Propositional_Cla", "Quantifiers_Cla", "Miniscope", "If", "Iff_Oracle" ]; (*regression test for locales -- sets several global flags!*) no_document use_thy "Locale_Test/Locale_Test";