diff -r 3f8b97ceedb2 -r cbedaddc9351 src/HOL/HOLCF/IOA/meta_theory/Pred.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Thu Dec 31 12:37:16 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(*  Title:      HOL/HOLCF/IOA/meta_theory/Pred.thy
-    Author:     Olaf Müller
-*)
-
-section \<open>Logical Connectives lifted to predicates\<close>
-
-theory Pred
-imports Main
-begin
-
-default_sort type
-
-type_synonym 'a predicate = "'a \<Rightarrow> bool"
-
-definition satisfies :: "'a \<Rightarrow> 'a predicate \<Rightarrow> bool"  ("_ \<Turnstile> _" [100,9] 8)
-  where "(s \<Turnstile> P) \<longleftrightarrow> P s"
-
-definition valid :: "'a predicate \<Rightarrow> bool"  (*  ("|-") *)
-  where "valid P \<longleftrightarrow> (\<forall>s. (s \<Turnstile> P))"
-
-definition NOT :: "'a predicate \<Rightarrow> 'a predicate"  ("\<^bold>\<not> _" [40] 40)
-  where "NOT P s \<longleftrightarrow> ~ (P s)"
-
-definition AND :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate"  (infixr "\<^bold>\<and>" 35)
-  where "(P \<^bold>\<and> Q) s \<longleftrightarrow> P s \<and> Q s"
-
-definition OR :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate"  (infixr "\<^bold>\<or>" 30)
-  where "(P \<^bold>\<or> Q) s \<longleftrightarrow> P s \<or> Q s"
-
-definition IMPLIES :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate"  (infixr "\<^bold>\<longrightarrow>" 25)
-  where "(P \<^bold>\<longrightarrow> Q) s \<longleftrightarrow> P s \<longrightarrow> Q s"
-
-end