| author | ballarin | 
| Tue, 31 Jul 2007 14:18:24 +0200 | |
| changeset 24087 | eb025d149a34 | 
| parent 13305 | f88d0c363582 | 
| permissions | -rw-r--r-- | 
| 9834 | 1 | use "../settings.ML"; | 
| 8745 | 2 | use_thy "Tree"; | 
| 9493 | 3 | use_thy "Tree2"; | 
| 13305 | 4 | use_thy "Plus"; | 
| 9721 | 5 | use_thy "case_exprs"; | 
| 8745 | 6 | use_thy "fakenat"; | 
| 7 | use_thy "natsum"; | |
| 8 | use_thy "pairs"; | |
| 10543 | 9 | use_thy "Option2"; | 
| 8745 | 10 | use_thy "types"; | 
| 11 | use_thy "prime_def"; | |
| 9844 | 12 | use_thy "simp"; | 
| 8745 | 13 | use_thy "Itrev"; | 
| 9644 | 14 | use_thy "AdvancedInd"; | 
| 10978 | 15 | use_thy "appendix"; |