# HG changeset patch
# User wenzelm
# Date 1404300191 -7200
# Node ID 58db442609ac705ca8cb1af0dd8359aa0d5c628d
# Parent  7806a74c54ac165237abd86f41c4176433803c89
modernized definitions;

diff -r 7806a74c54ac -r 58db442609ac src/HOL/UNITY/Detects.thy
--- a/src/HOL/UNITY/Detects.thy	Wed Jul 02 13:06:07 2014 +0200
+++ b/src/HOL/UNITY/Detects.thy	Wed Jul 02 13:23:11 2014 +0200
@@ -9,13 +9,11 @@
 
 theory Detects imports FP SubstAx begin
 
-consts
-   op_Detects  :: "['a set, 'a set] => 'a program set"  (infixl "Detects" 60)
-   op_Equality :: "['a set, 'a set] => 'a set"          (infixl "<==>" 60)
-   
-defs
-  Detects_def:  "A Detects B == (Always (-A \<union> B)) \<inter> (B LeadsTo A)"
-  Equality_def: "A <==> B == (-A \<union> B) \<inter> (A \<union> -B)"
+definition Detects :: "['a set, 'a set] => 'a program set"  (infixl "Detects" 60)
+  where "A Detects B = (Always (-A \<union> B)) \<inter> (B LeadsTo A)"
+
+definition Equality :: "['a set, 'a set] => 'a set"  (infixl "<==>" 60)
+  where "A <==> B = (-A \<union> B) \<inter> (A \<union> -B)"
 
 
 (* Corollary from Sectiom 3.6.4 *)