# HG changeset patch
# User blanchet
# Date 1315423881 -7200
# Node ID 19b70980a1bb3976c2de58ce20a15d9ed6920faa
# Parent  52318464c73b850f57b5e3810ddf2d2836210905
added new tagged encodings to Metis tests

diff -r 52318464c73b -r 19b70980a1bb src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Wed Sep 07 21:31:21 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Wed Sep 07 21:31:21 2011 +0200
@@ -34,8 +34,10 @@
    "poly_tags",
    "poly_tags?",
    "poly_tags??",
+   "poly_tags@?",
    "poly_tags!",
    "poly_tags!!",
+   "poly_tags@!",
    "poly_args",
    "raw_mono_guards",
    "raw_mono_guards?",
@@ -47,8 +49,10 @@
    "raw_mono_tags",
    "raw_mono_tags?",
    "raw_mono_tags??",
+   "raw_mono_tags@?",
    "raw_mono_tags!",
    "raw_mono_tags!!",
+   "raw_mono_tags@!",
    "raw_mono_args",
    "mono_guards",
    "mono_guards?",