quotient_def.ML
Sun, 06 Dec 2009 06:39:32 +0100 Cezary Kaliszyk Simpler definition code that works with any type maps.
Fri, 04 Dec 2009 21:42:55 +0100 Christian Urban not yet quite functional treatment of constants
Fri, 04 Dec 2009 15:19:39 +0100 Christian Urban merge
Thu, 03 Dec 2009 12:17:23 +0100 Cezary Kaliszyk Added the definition to quotient constant data.
Wed, 25 Nov 2009 21:48:32 +0100 Cezary Kaliszyk applic_prs
Wed, 25 Nov 2009 03:45:44 +0100 Christian Urban fixed the problem with generalising variables; at the moment it is quite a hack
Tue, 24 Nov 2009 15:31:29 +0100 Christian Urban use error instead of raising our own exception
Sun, 22 Nov 2009 15:30:23 +0100 Christian Urban updated to Isabelle 22nd November
Sat, 21 Nov 2009 23:23:01 +0100 Christian Urban slight tuning
Sat, 21 Nov 2009 11:16:48 +0100 Christian Urban tuned
Sat, 21 Nov 2009 10:58:08 +0100 Christian Urban tunded
Sat, 21 Nov 2009 02:49:39 +0100 Christian Urban simplified get_fun so that it uses directly rty and qty, instead of qenv
Thu, 19 Nov 2009 14:17:10 +0100 Christian Urban updated to new Isabelle
Wed, 18 Nov 2009 23:52:48 +0100 Christian Urban fixed the storage of qconst definitions
Thu, 12 Nov 2009 12:07:33 +0100 Christian Urban looking up data in quot_info works now (needs qualified string)
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.
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 13:47:04 +0100 Christian Urban removed typing information from get_fun in quotient_def; *potentially* dangerous
Thu, 05 Nov 2009 10:23:27 +0100 Christian Urban replaced check_term o parse_term by read_term
Thu, 05 Nov 2009 09:55:21 +0100 Christian Urban merged
Wed, 04 Nov 2009 12:19:04 +0100 Christian Urban more tuning
Wed, 04 Nov 2009 12:07:22 +0100 Christian Urban slightly tuned
Wed, 04 Nov 2009 11:59:15 +0100 Christian Urban separated the quotient_def into a separate file
less more (0) tip