src/HOL/Metis_Examples/Type_Encodings.thy
Thu, 01 Dec 2011 13:34:12 +0100 blanchet tuning
Wed, 16 Nov 2011 17:26:42 +0100 blanchet compile
Tue, 15 Nov 2011 12:39:29 +0100 huffman avoid theorem references like 'semiring_norm(111)'
Wed, 07 Sep 2011 21:31:21 +0200 blanchet added new tagged encodings to Metis tests
Wed, 07 Sep 2011 21:31:21 +0200 blanchet added new guards encoding to test
Wed, 07 Sep 2011 09:10:41 +0200 blanchet rationalize uniform encodings
Fri, 02 Sep 2011 14:43:20 +0200 blanchet renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
Tue, 30 Aug 2011 16:23:25 +0200 blanchet "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
Thu, 25 Aug 2011 14:25:07 +0200 blanchet rationalized option names -- mono becomes raw_mono and mangled becomes mono
Mon, 22 Aug 2011 15:02:45 +0200 blanchet include all encodings in tests, now that the incompleteness of some encodings has been addressed
Mon, 22 Aug 2011 15:02:45 +0200 blanchet made reconstruction of type tag equalities "\?x = \?x" reliable
Mon, 22 Aug 2011 15:02:45 +0200 blanchet clearer terminology
Tue, 26 Jul 2011 22:53:06 +0200 blanchet renamed "preds" encodings to "guards"
Fri, 01 Jul 2011 15:53:38 +0200 blanchet test a few more type encodings
Fri, 01 Jul 2011 15:53:38 +0200 blanchet renamed "type_sys" to "type_enc", which is more accurate
Mon, 06 Jun 2011 20:56:06 +0200 blanchet Metis code cleanup
Mon, 06 Jun 2011 20:36:35 +0200 blanchet compile
Mon, 06 Jun 2011 20:36:35 +0200 blanchet more preparations towards hijacking Metis
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuned Metis examples
less more (0) tip