Nominal/Ex/Lambda.thy
Sat, 14 May 2011 10:16:16 +0100 Christian Urban added a problem with inductive_cases (reported by Randy)
Tue, 03 May 2011 15:39:30 +0100 Christian Urban added two mutual recursive inductive definitions
Tue, 03 May 2011 13:09:08 +0100 Christian Urban proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
less more (0) -30 -10 -3 tip