# HG changeset patch
# User blanchet
# Date 1338971705 -7200
# Node ID 64025f5405a430298b23ddcb9a90caa5a2525ae4
# Parent  433787f8145e3bd9de8ea82f901821cfdf582563
removed killed encodings from Metis examples

diff -r 433787f8145e -r 64025f5405a4 src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Wed Jun 06 10:35:05 2012 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Wed Jun 06 10:35:05 2012 +0200
@@ -28,38 +28,24 @@
    "poly_guards?",
    "poly_guards??",
    (* "poly_guards@?", *)
-   "poly_guards!",
-   "poly_guards!!",
-   (* "poly_guards@!", *)
    "poly_tags",
    "poly_tags?",
    "poly_tags??",
-   "poly_tags!",
-   "poly_tags!!",
    "poly_args",
    "raw_mono_guards",
    "raw_mono_guards?",
    "raw_mono_guards??",
    "raw_mono_guards@?",
-   "raw_mono_guards!",
-   "raw_mono_guards!!",
-   "raw_mono_guards@!",
    "raw_mono_tags",
    "raw_mono_tags?",
    "raw_mono_tags??",
-   "raw_mono_tags!",
-   "raw_mono_tags!!",
    "raw_mono_args",
    "mono_guards",
    "mono_guards?",
    "mono_guards??",
-   "mono_guards!",
-   "mono_guards!!",
    "mono_tags",
    "mono_tags?",
    "mono_tags??",
-   "mono_tags!",
-   "mono_tags!!",
    "mono_args"]
 
 fun metis_exhaust_tac ctxt ths =