| author | haftmann | 
| Fri, 03 Dec 2010 14:22:24 +0100 | |
| changeset 40952 | 580b1a30994c | 
| parent 15494 | b09b68746eb6 | 
| child 41413 | 64cd30d6b0b8 | 
| permissions | -rw-r--r-- | 
| 15494 
b09b68746eb6
don't generate latex for LaTeXsugar and OptionalSugar
 kleing parents: 
15337diff
changeset | 1 | no_document use_thy "LaTeXsugar"; | 
| 
b09b68746eb6
don't generate latex for LaTeXsugar and OptionalSugar
 kleing parents: 
15337diff
changeset | 2 | no_document use_thy "OptionalSugar"; | 
| 15337 | 3 | use_thy "Sugar"; | 
| 4 |