src/HOL/Metis_Examples/Proxies.thy
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2015-10-02 blanchet 2015-10-02 adapted example
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2013-09-30 blanchet 2013-09-30 minor tweak to error message
2012-05-07 blanchet 2012-05-07 prevent spurious timeouts
2012-04-29 blanchet 2012-04-29 Sledgehammer can do it
2012-02-28 blanchet 2012-02-28 use SPASS instead of E for Metis examples -- it's seems faster for these small problems
2012-01-02 blanchet 2012-01-02 reintroduced Sledgehammer call taken out by 9bc924006136, with some hints to guide the naive relevance filter
2011-12-31 krauss 2011-12-31 disabled failing sledgehammer unit test (collateral damage of 184d36538e51)
2011-12-24 haftmann 2011-12-24 adjusted to set/pred distinction by means of type constructor `set`
2011-09-07 blanchet 2011-09-07 rationalize uniform encodings
2011-08-25 blanchet 2011-08-25 rationalized option names -- mono becomes raw_mono and mangled becomes mono
2011-07-26 blanchet 2011-07-26 renamed "preds" encodings to "guards"
2011-07-01 blanchet 2011-07-01 test a few more type encodings
2011-07-01 blanchet 2011-07-01 renamed "type_sys" to "type_enc", which is more accurate
2011-06-07 blanchet 2011-06-07 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
2011-06-06 blanchet 2011-06-06 generate less type information in polymorphic case
2011-06-06 blanchet 2011-06-06 Metis code cleanup
2011-06-06 blanchet 2011-06-06 more preparations towards hijacking Metis
2011-06-06 blanchet 2011-06-06 reintroduced metisFT in example
2011-06-06 blanchet 2011-06-06 tuned Metis examples