# HG changeset patch
# User blanchet
# Date 1309528418 -7200
# Node ID 030610b1e5a8feef5ef92a9921913ed3e96afbbb
# Parent  996b2022ff78f21f7b00f4817072a09cf49452a1
test a few more type encodings

diff -r 996b2022ff78 -r 030610b1e5a8 src/HOL/Metis_Examples/Proxies.thy
--- a/src/HOL/Metis_Examples/Proxies.thy	Fri Jul 01 15:53:38 2011 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy	Fri Jul 01 15:53:38 2011 +0200
@@ -50,7 +50,7 @@
 by linarith
 
 lemma "B \<subseteq> C"
-sledgehammer [type_enc = poly_args, max_relevant = 200, expect = some]
+sledgehammer [type_enc = poly_args, max_relevant = 100, expect = some]
 by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
 
 
diff -r 996b2022ff78 -r 030610b1e5a8 src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Fri Jul 01 15:53:38 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Fri Jul 01 15:53:38 2011 +0200
@@ -43,8 +43,8 @@
    "mangled_args",
    "simple",
    "poly_preds?",
-(* "poly_preds_heavy?", *)
-(* "poly_tags?", *)
+   "poly_preds_heavy?",
+   "poly_tags?",
 (* "poly_tags_heavy?", *)
    "mono_preds?",
    "mono_preds_heavy?",
@@ -56,9 +56,9 @@
    "mangled_tags_heavy?",
    "simple?",
    "poly_preds!",
-(* "poly_preds_heavy!", *)
+   "poly_preds_heavy!",
 (* "poly_tags!", *)
-(* "poly_tags_heavy!", *)
+   "poly_tags_heavy!",
    "mono_preds!",
    "mono_preds_heavy!",
    "mono_tags!",