| Thu, 12 Jun 2008 15:49:25 +0200 | nipkow | correction | changeset | files |
| Thu, 12 Jun 2008 14:46:15 +0200 | nipkow | tuned | changeset | files |
| Thu, 12 Jun 2008 14:33:28 +0200 | nipkow | Removed hide swap | changeset | files |
| Thu, 12 Jun 2008 14:21:10 +0200 | nipkow | fixed type | changeset | files |
| Thu, 12 Jun 2008 14:20:52 +0200 | nipkow | lemma modified | changeset | files |
| Thu, 12 Jun 2008 14:20:25 +0200 | nipkow | typo | changeset | files |
| Thu, 12 Jun 2008 14:20:07 +0200 | nipkow | had to add rule: because induct_tac no longer works correctly | changeset | files |
| Thu, 12 Jun 2008 14:10:41 +0200 | nipkow | Hid swap | changeset | files |
| Thu, 12 Jun 2008 11:51:47 +0200 | wenzelm | some reformatting; | changeset | files |
| Thu, 12 Jun 2008 10:03:45 +0200 | urbanc | added CK_Machine to the nominal section | changeset | files |
| Thu, 12 Jun 2008 09:56:28 +0200 | urbanc | soundness and completeness proofs for a CK machine as | changeset | files |
| Thu, 12 Jun 2008 09:41:13 +0200 | urbanc | emoved the parts that deal with the CK machine to a new theory | changeset | files |
| Thu, 12 Jun 2008 09:37:13 +0200 | urbanc | tuned header and comments | changeset | files |
| Wed, 11 Jun 2008 18:15:36 +0200 | wenzelm | OldGoals.inst; | changeset | files |
| Wed, 11 Jun 2008 18:04:02 +0200 | wenzelm | Drule.read_instantiate; | changeset | files |
| Wed, 11 Jun 2008 18:03:38 +0200 | wenzelm | qualified inst; | changeset | files |
| Wed, 11 Jun 2008 18:03:14 +0200 | wenzelm | qualified types_sorts, read_insts etc.; | changeset | files |
| Wed, 11 Jun 2008 18:02:50 +0200 | wenzelm | Drule.types_sorts; | changeset | files |
| Wed, 11 Jun 2008 18:02:25 +0200 | wenzelm | OldGoals.inst; | changeset | files |
| Wed, 11 Jun 2008 18:02:00 +0200 | wenzelm | Drule.read_instantiate; | changeset | files |
| Wed, 11 Jun 2008 18:01:36 +0200 | wenzelm | changed pred_congs: merely cover pred1_cong pred2_cong pred3_cong; | changeset | files |
| Wed, 11 Jun 2008 18:01:11 +0200 | wenzelm | removed obsolete/unused pred_congs; | changeset | files |
| Wed, 11 Jun 2008 15:41:57 +0200 | wenzelm | tuned comments; | changeset | files |
| Wed, 11 Jun 2008 15:41:33 +0200 | wenzelm | converted ML proofs from simpdata.ML; | changeset | files |
| Wed, 11 Jun 2008 15:41:08 +0200 | wenzelm | removed dead code; | changeset | files |
| Wed, 11 Jun 2008 15:40:44 +0200 | wenzelm | RuleInsts.res_inst_tac with proper context; | changeset | files |
| Wed, 11 Jun 2008 15:40:20 +0200 | wenzelm | more antiquotations; | changeset | files |
| Wed, 11 Jun 2008 11:20:10 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 11 Jun 2008 09:08:52 +0200 | haftmann | explicit rule for induct_tac | changeset | files |
| Tue, 10 Jun 2008 23:49:55 +0200 | wenzelm | tuned spacing; | changeset | files |