src/HOL/Metis_Examples/Type_Encodings.thy
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-02-14 blanchet 2014-02-14 merged 'List.map' and 'List.list.map'
2013-09-30 blanchet 2013-09-30 minor tweak to error message
2013-05-11 wenzelm 2013-05-11 avoid PolyML.makestring, even in dead code;
2013-01-03 blanchet 2013-01-03 use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
2012-08-03 blanchet 2012-08-03 never use MaSh in Metis examples, to avoid one dimension of nondeterminism
2012-06-26 blanchet 2012-06-26 reintroduced "t@" encoding, this time sound
2012-06-06 blanchet 2012-06-06 tweak Metis example to avoid glitch in proof reconstruction with a few guard-based, type-argument-less encodings
2012-06-06 blanchet 2012-06-06 added "args_query" encodings
2012-06-06 blanchet 2012-06-06 removed killed encodings from Metis examples
2012-03-20 blanchet 2012-03-20 take out experimental polymorphic @ encodings from Metis test -- proof reconstruction is fragile for them
2012-02-28 blanchet 2012-02-28 use SPASS instead of E for Metis examples -- it's seems faster for these small problems
2012-02-06 blanchet 2012-02-06 tuning
2012-01-30 blanchet 2012-01-30 example tuning
2011-12-21 blanchet 2011-12-21 removed killed encoding from example
2011-12-01 blanchet 2011-12-01 tuning
2011-11-16 blanchet 2011-11-16 compile
2011-11-15 huffman 2011-11-15 avoid theorem references like 'semiring_norm(111)'
2011-09-07 blanchet 2011-09-07 added new tagged encodings to Metis tests
2011-09-07 blanchet 2011-09-07 added new guards encoding to test
2011-09-07 blanchet 2011-09-07 rationalize uniform encodings
2011-09-02 blanchet 2011-09-02 renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
2011-08-30 blanchet 2011-08-30 "simple" was renamed "mono_simple" and there's now "poly_simple" as well -- but they are not needed here since for Metis they amount to the same as guards
2011-08-25 blanchet 2011-08-25 rationalized option names -- mono becomes raw_mono and mangled becomes mono
2011-08-22 blanchet 2011-08-22 include all encodings in tests, now that the incompleteness of some encodings has been addressed
2011-08-22 blanchet 2011-08-22 made reconstruction of type tag equalities "\?x = \?x" reliable
2011-08-22 blanchet 2011-08-22 clearer terminology
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-06 blanchet 2011-06-06 Metis code cleanup
2011-06-06 blanchet 2011-06-06 compile
2011-06-06 blanchet 2011-06-06 more preparations towards hijacking Metis
2011-06-06 blanchet 2011-06-06 tuned Metis examples