src/HOL/Transfer.thy
Tue, 17 Apr 2012 14:00:09 +0200 huffman make transfer method more deterministic by using SOLVED' on some subgoals
Tue, 17 Apr 2012 11:03:08 +0200 huffman add theory data for relator identity rules;
Wed, 04 Apr 2012 16:03:01 +0200 huffman add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
Tue, 03 Apr 2012 22:31:00 +0200 huffman new transfer proof method
less more (0) tip