# HG changeset patch # User blanchet # Date 1315423881 -7200 # Node ID d7094cae7df451bad264b6eff45c93646b8e827c # Parent 9e177ffe4745e1ccd87781b306e3d8a8109dff8a added new guards encoding to test diff -r 9e177ffe4745 -r d7094cae7df4 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 @@ -27,8 +27,10 @@ "poly_guards", "poly_guards?", "poly_guards??", + "poly_guards@?", "poly_guards!", "poly_guards!!", + "poly_guards@!", "poly_tags", "poly_tags?", "poly_tags??", @@ -38,8 +40,10 @@ "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??",