diff -r f04b33ce250f -r a4dc62a46ee4 IOA/meta_theory/Solve.thy
--- a/IOA/meta_theory/Solve.thy	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(*  Title:      HOL/IOA/meta_theory/Solve.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow & Konrad Slind
-    Copyright   1994  TU Muenchen
-
-Weak possibilities mapping (abstraction)
-*)
-
-Solve = IOA +
-
-consts
-
-  is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool"
-
-defs
-
-is_weak_pmap_def
-  "is_weak_pmap(f,C,A) ==                       
-   (!s:starts_of(C). f(s):starts_of(A)) &      
-   (!s t a. reachable(C,s) &                   
-            <s,a,t>:trans_of(C)                
-            --> if(a:externals(asig_of(C)),    
-                   <f(s),a,f(t)>:trans_of(A),  
-                   f(s)=f(t)))"
-
-end