Sat, 02 Oct 2010 17:50:33 -0700 huffman minimize theory imports
Fri, 01 Oct 2010 07:40:57 -0700 huffman added lemmas to List_Cpo.thy
Thu, 30 Sep 2010 19:42:12 -0700 huffman new_domain emits proper error message when a constructor argument type does not have sort 'rep'
Wed, 06 Oct 2010 17:56:41 +0200 blanchet move code from "Metis_Tactics" to "Metis_Reconstruct"
Wed, 06 Oct 2010 17:44:21 +0200 blanchet merged
Wed, 06 Oct 2010 17:44:07 +0200 blanchet qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)
Wed, 06 Oct 2010 17:42:57 +0200 blanchet get rid of function that duplicates existing Pure functionality
Wed, 06 Oct 2010 17:38:06 +0200 blanchet remove needless fact
Wed, 06 Oct 2010 12:01:55 +0200 blanchet added a few FIXMEs
Tue, 05 Oct 2010 12:50:45 +0200 blanchet tuned comments
Tue, 05 Oct 2010 12:06:08 +0200 blanchet document latest changes to Meson/Metis/Sledgehammer
Tue, 05 Oct 2010 12:04:57 +0200 blanchet remove needless Metis facts
Tue, 05 Oct 2010 12:04:49 +0200 blanchet hide one more name
Tue, 05 Oct 2010 12:04:19 +0200 blanchet qualify names
Tue, 05 Oct 2010 11:45:10 +0200 blanchet hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
Tue, 05 Oct 2010 11:14:56 +0200 blanchet clean up debugging output
Tue, 05 Oct 2010 11:10:37 +0200 blanchet factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
Tue, 05 Oct 2010 10:59:12 +0200 blanchet got rid of overkill "meson_choice" attribute;
Tue, 05 Oct 2010 10:30:50 +0200 blanchet more explicit name
Tue, 05 Oct 2010 10:28:11 +0200 blanchet factor out "Meson_Tactic" from "Meson_Clausify"
Mon, 04 Oct 2010 22:51:53 +0200 blanchet tuning
Mon, 04 Oct 2010 22:45:09 +0200 blanchet move Metis into Plain
Mon, 04 Oct 2010 22:01:34 +0200 blanchet added "Meson" theory to Makefile
Mon, 04 Oct 2010 21:57:23 +0200 blanchet update authors
Mon, 04 Oct 2010 21:55:54 +0200 blanchet remove Meson from Hilbert_Choice
Mon, 04 Oct 2010 21:50:32 +0200 blanchet remove Meson from Sledgehammer
Mon, 04 Oct 2010 21:49:07 +0200 blanchet move Meson to Plain
Mon, 04 Oct 2010 21:37:42 +0200 blanchet move MESON files together
Mon, 04 Oct 2010 20:55:55 +0200 blanchet paramify new skolems just like old ones (cf. reveal_old_skolem_terms)
Mon, 04 Oct 2010 18:31:34 +0200 blanchet fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
Mon, 04 Oct 2010 17:30:34 +0200 blanchet correctly handle multiple copies of the same axiom with the same types
Mon, 04 Oct 2010 16:36:20 +0200 blanchet put two operations in the right order
Mon, 04 Oct 2010 16:24:53 +0200 blanchet reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
Mon, 04 Oct 2010 15:05:19 +0200 blanchet apply "assume_tac" directly on the right assumption, using "rotate_tac" -- this ensures that the desired unifications are performed
Mon, 04 Oct 2010 14:36:18 +0200 blanchet instantiate foralls and release exists in the order described by the topological order
Mon, 04 Oct 2010 14:34:15 +0200 blanchet reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
Mon, 04 Oct 2010 09:08:46 +0200 blanchet renamed internal function
Mon, 04 Oct 2010 09:05:15 +0200 blanchet hack in MESON to make it less likely that variables (e.g. "x") get renamed (e.g. "xa") when resolving
Wed, 06 Oct 2010 13:48:12 +0200 haftmann tuned header
Tue, 05 Oct 2010 18:09:31 +0200 krauss tuned
Tue, 05 Oct 2010 18:09:29 +0200 krauss force less agressively
Tue, 05 Oct 2010 16:33:16 +0200 krauss lexicographic_order: replace parallel map with laziness to avoid wasting cycles on proofs that are not needed
Tue, 05 Oct 2010 14:19:43 +0200 krauss removed complicated (and rarely helpful) error reporting
Tue, 05 Oct 2010 14:19:40 +0200 krauss discontinued continuations to simplify control flow; dropped optimization in scnp
Tue, 05 Oct 2010 14:19:38 +0200 krauss use Cache structure instead of passing tables around explicitly
Tue, 05 Oct 2010 11:45:16 +0200 haftmann merged
Tue, 05 Oct 2010 11:37:42 +0200 haftmann lemmas fold_commute and fold_commute_apply
Fri, 07 May 2010 15:36:03 +0200 krauss spelling
Mon, 04 Oct 2010 14:46:49 +0200 haftmann adjusted to inductive characterization of sorted
Mon, 04 Oct 2010 14:46:49 +0200 haftmann tuned whitespace
Mon, 04 Oct 2010 14:46:48 +0200 haftmann turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
Mon, 04 Oct 2010 14:46:48 +0200 haftmann turned distinct and sorted into inductive predicates: yields nice induction principles for free
Mon, 04 Oct 2010 12:22:58 +0200 haftmann turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
Sat, 02 Oct 2010 12:32:31 +0200 blanchet some Poly/ML-specific debugging code escaped in the wild -- comment it out
Fri, 01 Oct 2010 22:44:36 +0200 haftmann merged
Fri, 01 Oct 2010 17:06:49 +0200 haftmann avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
Fri, 01 Oct 2010 17:06:49 +0200 haftmann moved ML_Context.value to Code_Runtime
Fri, 01 Oct 2010 16:05:25 +0200 haftmann constant `contents` renamed to `the_elem`
Fri, 01 Oct 2010 18:49:09 +0200 blanchet merged
Fri, 01 Oct 2010 18:48:37 +0200 blanchet tune whitespace
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip