--- 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"}))]
--- 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>