# HG changeset patch # User clasohm # Date 750875620 -3600 # Node ID da00b32c3977c95517edd3fbc612552d27e93264 # Parent 8dd033c3ffbce6dd259cc5a56f4a7f69797029a5 renamed: hol-rec.* to rec.*, lex-prod.* to lexprod.*, prop-log.* to pl.* diff -r 8dd033c3ffbc -r da00b32c3977 ex/ROOT.ML --- a/ex/ROOT.ML Sun Oct 17 17:23:51 1993 +0100 +++ b/ex/ROOT.ML Sun Oct 17 17:33:40 1993 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/ex/ROOT +(* Title: HOL/ex/ROOT ID: $Id$ Author: Tobias Nipkow, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge @@ -13,11 +13,11 @@ time_use "ex/cla.ML"; time_use "ex/meson.ML"; time_use "ex/meson-test.ML"; -time_use_thy "ex/lex-prod"; +time_use_thy "ex/lexprod"; time_use_thy "ex/puzzle"; time_use "ex/set.ML"; time_use_thy "ex/finite"; -time_use_thy "ex/prop-log"; +time_use_thy "ex/pl"; time_use_thy "ex/term"; time_use_thy "ex/simult"; maketest "END: Root file for HOL examples";