# HG changeset patch
# User urbanc
# Date 1303179921 0
# Node ID d8d1e1f53d6e4c76ce5565f254dc0aafc40acd74
# Parent  7c68b9ad448656c134dd5f2f54722d4452db797e
removed experimental code from Matcher

diff -r 7c68b9ad4486 -r d8d1e1f53d6e Matcher.thy
--- a/Matcher.thy	Tue Apr 19 02:19:56 2011 +0000
+++ b/Matcher.thy	Tue Apr 19 02:25:21 2011 +0000
@@ -2,15 +2,6 @@
   imports "Main" 
 begin
 
-term "TYPE (nat * int)"
-term "TYPE ('a)"
-
-definition
-  P:: "'a itself \<Rightarrow> bool"
-where
-  "P (TYPE ('a)) \<equiv> ((\<lambda>x. (x::'a)) = (\<lambda>x. x))"
-
-
 section {* Sequential Composition of Sets *}
 
 definition