# HG changeset patch # User blanchet # Date 1332247989 -3600 # Node ID 3347c853d8e2bd7554af32932bb22f22f5b00347 # Parent 10bece4ac87ea8153ebcbef61737106647f5b5cd take out experimental polymorphic @ encodings from Metis test -- proof reconstruction is fragile for them diff -r 10bece4ac87e -r 3347c853d8e2 src/HOL/Metis_Examples/Type_Encodings.thy --- a/src/HOL/Metis_Examples/Type_Encodings.thy Tue Mar 20 13:53:09 2012 +0100 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Tue Mar 20 13:53:09 2012 +0100 @@ -27,10 +27,10 @@ "poly_guards", "poly_guards?", "poly_guards??", - "poly_guards@?", + (* "poly_guards@?", *) "poly_guards!", "poly_guards!!", - "poly_guards@!", + (* "poly_guards@!", *) "poly_tags", "poly_tags?", "poly_tags??",