nipkow [Thu, 12 Jun 2008 14:46:15 +0200] rev 27171
tuned
nipkow [Thu, 12 Jun 2008 14:33:28 +0200] rev 27170
Removed hide swap
nipkow [Thu, 12 Jun 2008 14:21:10 +0200] rev 27169
fixed type
nipkow [Thu, 12 Jun 2008 14:20:52 +0200] rev 27168
lemma modified
nipkow [Thu, 12 Jun 2008 14:20:25 +0200] rev 27167
typo
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;
wenzelm [Wed, 11 Jun 2008 18:03:14 +0200] rev 27156
qualified types_sorts, read_insts etc.;
wenzelm [Wed, 11 Jun 2008 18:02:50 +0200] rev 27155
Drule.types_sorts;
wenzelm [Wed, 11 Jun 2008 18:02:25 +0200] rev 27154
OldGoals.inst;
wenzelm [Wed, 11 Jun 2008 18:02:00 +0200] rev 27153
Drule.read_instantiate;
wenzelm [Wed, 11 Jun 2008 18:01:36 +0200] rev 27152
changed pred_congs: merely cover pred1_cong pred2_cong pred3_cong;
wenzelm [Wed, 11 Jun 2008 18:01:11 +0200] rev 27151
removed obsolete/unused pred_congs;
wenzelm [Wed, 11 Jun 2008 15:41:57 +0200] rev 27150
tuned comments;
wenzelm [Wed, 11 Jun 2008 15:41:33 +0200] rev 27149
converted ML proofs from simpdata.ML;
tuned;
wenzelm [Wed, 11 Jun 2008 15:41:08 +0200] rev 27148
removed dead code;