Fri, 10 Nov 2000 19:10:34 +0100 | wenzelm | has_meta_prems: include "=="; | changeset | files |
Fri, 10 Nov 2000 19:09:40 +0100 | wenzelm | store_standard_thm "norm_hhf_eq"; | changeset | files |
Fri, 10 Nov 2000 19:08:30 +0100 | wenzelm | proper theory context for mesontest2; | changeset | files |
Fri, 10 Nov 2000 19:07:17 +0100 | wenzelm | inductive_rulify2 accomodates malformed induction rules; | changeset | files |
Fri, 10 Nov 2000 19:06:54 +0100 | wenzelm | Sign.certify_tycon, Sign.certify_const; | changeset | files |
Fri, 10 Nov 2000 19:06:30 +0100 | wenzelm | improved cong_definition theorems; | changeset | files |