isabelle: Changelog

nipkow [Thu, 12 Jun 2008 14:20:07 +0200] rev 27166

had to add rule: because induct_tac no longer works correctly

nipkow [Thu, 12 Jun 2008 14:10:41 +0200] rev 27165

Hid swap

wenzelm [Thu, 12 Jun 2008 11:51:47 +0200] rev 27164

some reformatting;

urbanc [Thu, 12 Jun 2008 10:03:45 +0200] rev 27163

added CK_Machine to the nominal section

urbanc [Thu, 12 Jun 2008 09:56:28 +0200] rev 27162

soundness and completeness proofs for a CK machine as well as proofs for type preservation

urbanc [Thu, 12 Jun 2008 09:41:13 +0200] rev 27161

emoved the parts that deal with the CK machine to a new theory

urbanc [Thu, 12 Jun 2008 09:37:13 +0200] rev 27160

tuned header and comments

wenzelm [Wed, 11 Jun 2008 18:15:36 +0200] rev 27159

OldGoals.inst;

wenzelm [Wed, 11 Jun 2008 18:04:02 +0200] rev 27158

Drule.read_instantiate; Drule.types_sorts;

wenzelm [Wed, 11 Jun 2008 18:03:38 +0200] rev 27157

qualified inst;

isabelle