| author | huffman | 
| Tue, 24 Feb 2009 08:20:14 -0800 | |
| changeset 30080 | 4cf42465b3da | 
| 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"; |