changeset 33615 | 261abc2e3155 |
parent 29921 | 3d50e96bcd6b |
child 35707 | 44936737902d |
--- a/src/HOLCF/ROOT.ML Wed Nov 11 09:02:37 2009 +0100 +++ b/src/HOLCF/ROOT.ML Wed Nov 11 14:15:11 2009 +0100 @@ -1,10 +1,9 @@ (* Title: HOLCF/ROOT.ML - ID: $Id$ Author: Franz Regensburger HOLCF -- a semantic extension of HOL by the LCF logic. *) -no_document use_thy "Nat_Int_Bij"; +no_document use_thys ["Nat_Int_Bij"]; -use_thy "HOLCF"; +use_thys ["HOLCF"];