Tue, 16 Oct 2001 17:58:13 +0200 | wenzelm | tuned induction proofs; | changeset | files |
Tue, 16 Oct 2001 17:56:12 +0200 | wenzelm | dest_env: norm_term on rhs; | changeset | files |
Tue, 16 Oct 2001 17:55:53 +0200 | wenzelm | typedef: export result; | changeset | files |
Tue, 16 Oct 2001 17:55:38 +0200 | wenzelm | ignore typedef result; | changeset | files |
Tue, 16 Oct 2001 17:55:16 +0200 | wenzelm | declare projected induction rules stemming from nested recursion; | changeset | files |
Tue, 16 Oct 2001 17:52:07 +0200 | wenzelm | TypedefPackage.add_typedef_no_result; | changeset | files |