src/HOL/Tools/Meson/meson_clausify.ML
Wed, 23 Mar 2011 10:18:42 +0100 blanchet avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
Fri, 17 Dec 2010 13:45:43 +0100 wenzelm refer to regular structure Simplifier;
Fri, 29 Oct 2010 12:49:05 +0200 blanchet restructure Skolemization code slightly
Fri, 29 Oct 2010 12:49:05 +0200 blanchet ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
Fri, 29 Oct 2010 12:49:05 +0200 blanchet more work on new Skolemizer without Hilbert_Choice
Fri, 29 Oct 2010 12:49:05 +0200 blanchet fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
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)
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 21:49:07 +0200 blanchet move Meson to Plain
Mon, 04 Oct 2010 21:37:42 +0200 blanchet move MESON files together
less more (0) tip