| author | huffman | 
| Wed, 04 Apr 2012 13:41:38 +0200 | |
| changeset 47350 | ec46b60aa582 | 
| 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"; |