# HG changeset patch
# User wenzelm
# Date 1444504357 -7200
# Node ID 509d7ee638f8ce684235371a42988e611ac636d5
# Parent  92e97b800d1e07ae4c532eafa41aa96c8d6ab5bb
tuned;

diff -r 92e97b800d1e -r 509d7ee638f8 src/Cube/Cube.thy
--- a/src/Cube/Cube.thy	Sat Oct 10 21:08:58 2015 +0200
+++ b/src/Cube/Cube.thy	Sat Oct 10 21:12:37 2015 +0200
@@ -48,9 +48,6 @@
   "\<^bold>\<lambda>x:A. B" \<rightleftharpoons> "CONST Abs(A, \<lambda>x. B)"
   "\<Prod>x:A. B" \<rightharpoonup> "CONST Prod(A, \<lambda>x. B)"
   "A \<rightarrow> B" \<rightharpoonup> "CONST Prod(A, \<lambda>_. B)"
-
-syntax
-  "_Pi" :: "[idt, term, term] \<Rightarrow> term"    ("(3\<Prod>_:_./ _)" [0, 0] 10)
 print_translation \<open>
   [(@{const_syntax Prod},
     fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
diff -r 92e97b800d1e -r 509d7ee638f8 src/Cube/Example.thy
--- a/src/Cube/Example.thy	Sat Oct 10 21:08:58 2015 +0200
+++ b/src/Cube/Example.thy	Sat Oct 10 21:12:37 2015 +0200
@@ -19,7 +19,7 @@
 
 method_setup strip_asms =
   \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts =>
-    REPEAT (resolve_tac ctxt [@{thm strip_b}, @{thm strip_s}] 1 THEN
+    REPEAT (resolve_tac ctxt @{thms strip_b strip_s} 1 THEN
     DEPTH_SOLVE_1 (assume_tac ctxt 1 ORELSE resolve_tac ctxt (facts @ thms) 1))))\<close>