author | nipkow |
Tue, 05 Sep 2000 09:03:17 +0200 | |
changeset 9834 | 109b11c4e77e |
parent 9722 | a5f86aed785b |
child 9844 | 8016321c7de1 |
permissions | -rw-r--r-- |
use "../settings.ML"; use_thy "Tree"; use_thy "Tree2"; use_thy "case_exprs"; use_thy "fakenat"; use_thy "natsum"; use_thy "arith1"; use_thy "arith2"; use_thy "arith3"; use_thy "arith4"; use_thy "pairs"; use_thy "types"; use_thy "prime_def"; use_thy "def_rewr"; use_thy "let_rewr"; use_thy "cond_rewr"; use_thy "case_splits"; use_thy "trace_simp"; use_thy "Itrev"; use_thy "AdvancedInd"; use_thy "asm_simp";