take out experimental polymorphic @ encodings from Metis test -- proof reconstruction is fragile for them
authorblanchet
Tue, 20 Mar 2012 13:53:09 +0100
changeset 47048 3347c853d8e2
parent 47047 10bece4ac87e
child 47049 72bd3311ecba
take out experimental polymorphic @ encodings from Metis test -- proof reconstruction is fragile for them
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??",