QuotMain.thy
Sat, 21 Nov 2009 13:14:35 +0100 Christian Urban my first version of repabs injection
Sat, 21 Nov 2009 11:16:48 +0100 Christian Urban tuned
Sat, 21 Nov 2009 03:12:50 +0100 Christian Urban tuned
Sat, 21 Nov 2009 02:49:39 +0100 Christian Urban simplified get_fun so that it uses directly rty and qty, instead of qenv
Fri, 20 Nov 2009 13:03:01 +0100 Christian Urban started regularize of rtrm/qtrm version; looks quite promising
Thu, 19 Nov 2009 14:17:10 +0100 Christian Urban updated to new Isabelle
Fri, 13 Nov 2009 16:44:36 +0100 Christian Urban added some tracing information to all phases of lifting to the function lift_thm
Thu, 12 Nov 2009 13:56:07 +0100 Cezary Kaliszyk merged
Thu, 12 Nov 2009 02:54:40 +0100 Christian Urban changed the quotdata to be a symtab table (needs fixing)
Thu, 12 Nov 2009 02:18:36 +0100 Christian Urban added a container for quotient constants (does not work yet though)
Wed, 11 Nov 2009 18:49:46 +0100 Cezary Kaliszyk Modifications while preparing the goal-directed version.
Tue, 10 Nov 2009 09:32:16 +0100 Cezary Kaliszyk More code cleaning and commenting
Mon, 09 Nov 2009 15:40:43 +0100 Cezary Kaliszyk Minor cleaning and removing of some 'handle _'.
Mon, 09 Nov 2009 15:23:33 +0100 Cezary Kaliszyk Cleaning and commenting
Mon, 09 Nov 2009 13:47:46 +0100 Cezary Kaliszyk Fixes for the other get_fun implementation.
Fri, 06 Nov 2009 19:26:08 +0100 Christian Urban updated to new Isabelle version and added a new example file
Fri, 06 Nov 2009 09:48:37 +0100 Christian Urban tuned the code in quotient and quotient_def
Thu, 05 Nov 2009 16:43:57 +0100 Cezary Kaliszyk More functionality for lifting list.cases and list.recs.
Thu, 05 Nov 2009 13:36:46 +0100 Cezary Kaliszyk Remaining fixes for polymorphic types. map_append now lifts properly with 'a list and 'b list.
Thu, 05 Nov 2009 10:46:54 +0100 Christian Urban removed Simplifier.context
Thu, 05 Nov 2009 09:55:21 +0100 Christian Urban merged
Thu, 05 Nov 2009 09:38:34 +0100 Cezary Kaliszyk Infrastructure for polymorphic types
Wed, 04 Nov 2009 15:27:32 +0100 Cezary Kaliszyk Type instantiation in regularize
Wed, 04 Nov 2009 14:03:46 +0100 Cezary Kaliszyk Description of regularize
Wed, 04 Nov 2009 11:59:15 +0100 Christian Urban separated the quotient_def into a separate file
Wed, 04 Nov 2009 10:43:33 +0100 Christian Urban fixed definition of PLUS
Wed, 04 Nov 2009 10:31:20 +0100 Christian Urban simplified the quotient_def code
Wed, 04 Nov 2009 09:52:31 +0100 Cezary Kaliszyk Lifting 'fold1.simps(2)' and some cleaning.
Tue, 03 Nov 2009 17:30:43 +0100 Cezary Kaliszyk merge
Tue, 03 Nov 2009 17:30:27 +0100 Cezary Kaliszyk applic_prs
less more (0) -100 -50 -30 tip