# HG changeset patch
# User ballarin
# Date 1227632809 -3600
# Node ID 9cb1297b6f139446c5ef74d5941ec72e2b7a747b
# Parent  6f6bf52e75bb6c3a49240550931d9f3ec1671748
Test for term patterns added.

diff -r 6f6bf52e75bb -r 9cb1297b6f13 src/FOL/ex/NewLocaleTest.thy
--- a/src/FOL/ex/NewLocaleTest.thy	Tue Nov 25 18:06:21 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Tue Nov 25 18:06:49 2008 +0100
@@ -140,4 +140,27 @@
 end
 print_locale! rgrp
 
+
+text {* Patterns *}
+
+lemma (in rgrp)
+  assumes "y ** x = z ** x" (is ?a)
+  shows "y = z" (is ?t)
+proof -
+  txt {* Weird proof involving patterns from context element and conclusion. *}
+  {
+    assume ?a
+    then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
+      by (simp add: assoc [symmetric])
+    then have ?t by (simp add: rone rinv)
+  }
+  note x = this
+  show ?t by (rule x [OF `?a`])
+qed
+
+lemma
+  assumes "P <-> P" (is "?p <-> _")
+  shows "?p <-> ?p"
+  .
+
 end