| Fri, 10 Nov 2000 19:15:14 +0100 | wenzelm | use inverse, divide from basic HOL; | changeset | files |
| Fri, 10 Nov 2000 19:13:29 +0100 | wenzelm | norm_hhf_tac; | changeset | files |
| Fri, 10 Nov 2000 19:13:01 +0100 | wenzelm | rewrite_goal_tac moved to tactic.ML; | changeset | files |
| Fri, 10 Nov 2000 19:12:30 +0100 | wenzelm | added rewrite_goal_tac; | changeset | files |
| Fri, 10 Nov 2000 19:11:51 +0100 | wenzelm | added certify_tycon, certify_tyabbr, certify_const; | changeset | files |
| 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 |
| Fri, 10 Nov 2000 19:05:28 +0100 | wenzelm | simplified induction; | changeset | files |
| Fri, 10 Nov 2000 19:04:31 +0100 | wenzelm | added axclass power (from HOL.thy); | changeset | files |
| Fri, 10 Nov 2000 19:03:55 +0100 | wenzelm | simplified atomize; | changeset | files |
| Fri, 10 Nov 2000 19:03:06 +0100 | wenzelm | axclass power moved to Nat.thy; | changeset | files |
| Fri, 10 Nov 2000 19:02:37 +0100 | wenzelm | added axclass inverse and consts inverse, divide (infix "/"); | changeset | files |
| Fri, 10 Nov 2000 19:01:33 +0100 | wenzelm | FOL_basic_ss: simprocs moved to FOL_ss; | changeset | files |
| Fri, 10 Nov 2000 19:00:51 +0100 | wenzelm | added atomize_eq; | changeset | files |
| Fri, 10 Nov 2000 19:00:22 +0100 | wenzelm | val atomize = thms "atomize'"; | changeset | files |
| Fri, 10 Nov 2000 16:31:28 +0100 | nipkow | > etc | changeset | files |
| Fri, 10 Nov 2000 16:26:44 +0100 | nipkow | new: > and >= | changeset | files |
| Fri, 10 Nov 2000 15:05:09 +0100 | nipkow | rule inversion | changeset | files |
| Fri, 10 Nov 2000 09:17:54 +0100 | nipkow | JMB -> JMPB. Email von Johannes Pfeifroth. | changeset | files |
| Thu, 09 Nov 2000 21:38:30 +0100 | wenzelm | updated; | changeset | files |
| Thu, 09 Nov 2000 21:38:00 +0100 | wenzelm | fixed \title: convert "_" to "-"; | changeset | files |
| Wed, 08 Nov 2000 23:04:54 +0100 | wenzelm | tuned isabelle environment; | changeset | files |
| Wed, 08 Nov 2000 17:46:24 +0100 | nipkow | subgoals | changeset | files |
| Wed, 08 Nov 2000 14:38:04 +0100 | nipkow | *** empty log message *** | changeset | files |