src/HOL/Transfer.thy
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Wed, 16 May 2012 19:17:20 +0200 kuncar generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
Tue, 15 May 2012 11:50:34 +0200 huffman add transfer rules for nat_rec and funpow
Fri, 27 Apr 2012 14:07:31 +0200 huffman implement transfer tactic with more scalable forward proof methods
Sun, 22 Apr 2012 21:32:35 +0200 huffman tuned precedence order of transfer rules
Sun, 22 Apr 2012 11:05:04 +0200 huffman new example theory for quotient/transfer
Sat, 21 Apr 2012 20:52:33 +0200 huffman enable variant of transfer method that proves an implication instead of an equivalence
Fri, 20 Apr 2012 22:05:07 +0200 huffman add transfer rule for nat_case
Fri, 20 Apr 2012 22:54:13 +0200 huffman uniform naming scheme for transfer rules
Fri, 20 Apr 2012 22:49:40 +0200 huffman rename 'correspondence' method to 'transfer_prover'
Fri, 20 Apr 2012 15:49:45 +0200 huffman add secondary transfer rule for universal quantifiers on non-bi-total relations
Fri, 20 Apr 2012 15:30:13 +0200 huffman add transfer rule for 'id'
Fri, 20 Apr 2012 10:18:08 +0200 huffman make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
Thu, 19 Apr 2012 19:36:09 +0200 huffman add transfer rule for Let
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