| author | huffman | 
| Fri, 24 Feb 2012 13:37:23 +0100 | |
| changeset 46647 | de514a98f6b6 | 
| parent 41413 | 64cd30d6b0b8 | 
| permissions | -rw-r--r-- | 
| 41413 
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
 wenzelm parents: 
15494diff
changeset | 1 | no_document use_thys [ | 
| 
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
 wenzelm parents: 
15494diff
changeset | 2 | "~~/src/HOL/Library/LaTeXsugar", | 
| 
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
 wenzelm parents: 
15494diff
changeset | 3 | "~~/src/HOL/Library/OptionalSugar" | 
| 
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
 wenzelm parents: 
15494diff
changeset | 4 | ]; | 
| 15337 | 5 | use_thy "Sugar"; | 
| 6 |