"simple" was renamed "mono_simple" and there's now "poly_simple" as well -- but they are not needed here since for Metis they amount to the same as guards
authorblanchet
Tue, 30 Aug 2011 16:23:25 +0200
changeset 44598 b054ca3f07b5
parent 44597 03bbadb252db
child 44599 d34ff13371e0
"simple" was renamed "mono_simple" and there's now "poly_simple" as well -- but they are not needed here since for Metis they amount to the same as guards
src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Tue Aug 30 16:11:42 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Tue Aug 30 16:23:25 2011 +0200
@@ -39,7 +39,6 @@
    "mono_tags",
    "mono_tags_uniform",
    "mono_args",
-   "simple",
    "poly_guards?",
    "poly_guards_uniform?",
    "poly_tags?",
@@ -52,7 +51,6 @@
    "mono_guards_uniform?",
    "mono_tags?",
    "mono_tags_uniform?",
-   "simple?",
    "poly_guards!",
    "poly_guards_uniform!",
    "poly_tags!",
@@ -64,8 +62,7 @@
    "mono_guards!",
    "mono_guards_uniform!",
    "mono_tags!",
-   "mono_tags_uniform!",
-   "simple!"]
+   "mono_tags_uniform!"]
 
 fun metis_exhaust_tac ctxt ths =
   let