# HG changeset patch
# User blanchet
# Date 1324488188 -3600
# Node ID e49e45fee615ad4cc6391123163f37f6c0e93c3c
# Parent  87a446a6496db6a26bbe4ef7f32875372a65014b
removed killed encoding from example

diff -r 87a446a6496d -r e49e45fee615 src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Wed Dec 21 15:04:28 2011 +0100
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Wed Dec 21 18:23:08 2011 +0100
@@ -33,10 +33,8 @@
    "poly_tags",
    "poly_tags?",
    "poly_tags??",
-   "poly_tags@?",
    "poly_tags!",
    "poly_tags!!",
-   "poly_tags@!",
    "poly_args",
    "raw_mono_guards",
    "raw_mono_guards?",
@@ -48,10 +46,8 @@
    "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?",