src/HOL/TLA/Memory/ROOT.ML
changeset 6255 db63752140c7
parent 3823 071c87125cea
child 9000 c20d58286a51
     1.1 --- a/src/HOL/TLA/Memory/ROOT.ML	Mon Feb 08 13:02:42 1999 +0100
     1.2 +++ b/src/HOL/TLA/Memory/ROOT.ML	Mon Feb 08 13:02:56 1999 +0100
     1.3 @@ -1,2 +1,2 @@
     1.4  
     1.5 -use_thy "Memory";
     1.6 +use_thy "MemoryImplementation";