| author | haftmann | 
| Wed, 22 Sep 2010 18:40:35 +0200 | |
| changeset 39642 | dd7b582f6929 | 
| 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 |