| author | haftmann | 
| Mon, 30 Aug 2010 15:01:32 +0200 | |
| changeset 38909 | 919c924067f3 | 
| parent 15494 | b09b68746eb6 | 
| child 41413 | 64cd30d6b0b8 | 
| permissions | -rw-r--r-- | 
| 
15494
 
b09b68746eb6
don't generate latex for LaTeXsugar and OptionalSugar
 
kleing 
parents: 
15337 
diff
changeset
 | 
1  | 
no_document use_thy "LaTeXsugar";  | 
| 
 
b09b68746eb6
don't generate latex for LaTeXsugar and OptionalSugar
 
kleing 
parents: 
15337 
diff
changeset
 | 
2  | 
no_document use_thy "OptionalSugar";  | 
| 15337 | 3  | 
use_thy "Sugar";  | 
4  |