| author | wenzelm | 
| Sat, 03 Nov 2001 01:39:17 +0100 | |
| changeset 12028 | 52aa183c15bb | 
| parent 11398 | d7711be8c3a9 | 
| child 16966 | 37e34f315057 | 
| permissions | -rw-r--r-- | 
| 11398 
d7711be8c3a9
Library/ROOT.ML moved to Library/Library/ROOT.ML to avoid accidential
 wenzelm parents: diff
changeset | 1 | use_thy "Library"; |