Wed, 19 Jan 2011 19:06:52 +0100 Christian Urban base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Wed, 19 Jan 2011 18:56:28 +0100 Christian Urban ported some of the old proofs to serve as testcases
Wed, 19 Jan 2011 18:07:29 +0100 Christian Urban added eqvt and supp lemma for removeAll (function from List.thy)
Wed, 19 Jan 2011 17:54:50 +0100 Christian Urban theory name as it should be
Wed, 19 Jan 2011 17:54:06 +0100 Christian Urban removed diagnostic code
Wed, 19 Jan 2011 17:11:10 +0100 Christian Urban added Minimal file to test things
Wed, 19 Jan 2011 07:06:47 +0100 Christian Urban defined height as a function that returns an integer
Tue, 18 Jan 2011 21:28:07 +0100 Christian Urban deleted diagnostic code
Tue, 18 Jan 2011 21:26:58 +0100 Christian Urban some tryes about substitution over type-schemes
Tue, 18 Jan 2011 19:27:30 +0100 Christian Urban defined properly substitution
Tue, 18 Jan 2011 18:04:40 +0100 Christian Urban derived stronger Abs_eq_iff2 theorems
Tue, 18 Jan 2011 17:30:47 +0100 Christian Urban made alpha_abs_set_stronger1 stronger
(0) -1000 -300 -100 -12 +12 +100 +300 tip