src/HOL/Lifting.thy
Sat, 21 Apr 2012 13:12:27 +0200 huffman move alternative definition lemmas into Lifting.thy;
Sat, 21 Apr 2012 13:06:22 +0200 huffman tuned proofs
Thu, 19 Apr 2012 08:45:13 +0200 huffman generate abs_induct rules for quotient types
Wed, 18 Apr 2012 17:04:03 +0200 kuncar Lifting: generate more thms & note them & tuned
Wed, 18 Apr 2012 15:48:32 +0200 huffman move constant 'Respects' into Lifting.thy;
Wed, 18 Apr 2012 15:09:07 +0200 huffman add lemma Quotient_abs_induct
Wed, 18 Apr 2012 14:59:04 +0200 huffman more usage of context blocks
Wed, 18 Apr 2012 14:34:25 +0200 huffman use context block
Wed, 18 Apr 2012 12:15:20 +0200 huffman lifting_setup generates transfer rule for rep of typedefs
Wed, 18 Apr 2012 10:52:49 +0200 huffman use context block to organize typedef lifting theorems
Tue, 17 Apr 2012 19:16:13 +0200 kuncar tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
Mon, 16 Apr 2012 20:50:43 +0200 kuncar leave Lifting prefix
Thu, 12 Apr 2012 11:01:15 +0200 bulwahn merged
Wed, 04 Apr 2012 15:15:48 +0900 griff manual merge
Thu, 05 Apr 2012 15:59:25 +0200 huffman add transfer lemmas for quotients
Wed, 04 Apr 2012 20:45:19 +0200 huffman merged
Wed, 04 Apr 2012 16:48:39 +0200 huffman add lemmas for generating transfer rules for typedefs
Wed, 04 Apr 2012 17:51:12 +0200 kuncar support non-open typedefs; define cr_rel in terms of a rep function for typedefs
Wed, 04 Apr 2012 12:25:58 +0200 huffman update keywords file
Wed, 04 Apr 2012 13:42:01 +0200 huffman lift_definition command generates transfer rule
Tue, 03 Apr 2012 22:31:00 +0200 huffman new transfer proof method
Tue, 03 Apr 2012 16:26:48 +0200 kuncar new package Lifting - initial commit
less more (0) tip