| author | blanchet | 
| Tue, 03 Jan 2012 18:33:17 +0100 | |
| changeset 46082 | 1c436a920730 | 
| 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 |