--- 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 =