src/HOL/Tools/Metis/metis_generate.ML
2015-06-02 wenzelm 2015-06-02 clarified context;
2015-03-31 wenzelm 2015-03-31 more standard Long_Name operations;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-06-27 blanchet 2014-06-27 tuned whitespace and parentheses
2014-06-16 blanchet 2014-06-16 simplified code
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-09-09 blanchet 2013-09-09 move metis to new monomorphizer
2013-05-26 blanchet 2013-05-26 handle lambda-lifted problems in Isar construction code
2013-05-16 blanchet 2013-05-16 tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-05-15 blanchet 2013-05-15 renamed Sledgehammer functions with 'for' in their names to 'of'
2013-03-28 boehmes 2013-03-28 new, simpler implementation of monomorphization; old monomorphization code is still available as Legacy_Monomorphization; modified SMT integration to use the new monomorphization code
2012-12-13 blanchet 2012-12-13 generate comments with original names for debugging
2012-06-26 blanchet 2012-06-26 added type arguments to "ATerm" constructor -- but don't use them yet
2012-06-26 blanchet 2012-06-26 started adding polymophic SPASS output
2012-06-26 blanchet 2012-06-26 tuning
2012-05-21 blanchet 2012-05-21 add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
2012-05-13 blanchet 2012-05-13 get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
2012-03-20 blanchet 2012-03-20 remove two options that were found to play hardly any role
2012-03-20 blanchet 2012-03-20 added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
2012-02-04 blanchet 2012-02-04 made option available to users (mostly for experiments)
2012-01-30 blanchet 2012-01-30 rename lambda translation schemes
2012-01-26 blanchet 2012-01-26 separate orthogonal components
2012-01-23 blanchet 2012-01-23 renamed two files to make room for a new file