# HG changeset patch
# User wenzelm
# Date 1441205057 -7200
# Node ID 896989117ce0d0704ef9f6fdbf2847a04ca7e6d4
# Parent  42c2698d2273c7665951248e905a2596cd66218d
eliminated old 'defs';

diff -r 42c2698d2273 -r 896989117ce0 src/ZF/UNITY/UNITY.thy
--- a/src/ZF/UNITY/UNITY.thy	Wed Sep 02 16:01:57 2015 +0200
+++ b/src/ZF/UNITY/UNITY.thy	Wed Sep 02 16:44:17 2015 +0200
@@ -12,10 +12,6 @@
 
 This ZF theory was ported from its HOL equivalent.\<close>
 
-consts
-  "constrains" :: "[i, i] => i"  (infixl "co"     60)
-  op_unless    :: "[i, i] => i"  (infixl "unless" 60)
-
 definition
   program  :: i  where
   "program == {<init, acts, allowed>:
@@ -72,6 +68,14 @@
   initially :: "i=>i"  where
   "initially(A) == {F \<in> program. Init(F)\<subseteq>A}"
 
+definition "constrains" :: "[i, i] => i"  (infixl "co" 60)  where
+  "A co B == {F \<in> program. (\<forall>act \<in> Acts(F). act``A\<subseteq>B) & st_set(A)}"
+    --\<open>the condition @{term "st_set(A)"} makes the definition slightly
+         stronger than the HOL one\<close>
+
+definition unless :: "[i, i] => i"  (infixl "unless" 60)  where
+  "A unless B == (A - B) co (A \<union> B)"
+
 definition
   stable     :: "i=>i"  where
    "stable(A) == A co A"
@@ -93,15 +97,6 @@
   pg_compl :: "i=>i"  where
   "pg_compl(X)== program - X"
 
-defs
-  constrains_def:
-     "A co B == {F \<in> program. (\<forall>act \<in> Acts(F). act``A\<subseteq>B) & st_set(A)}"
-    --\<open>the condition @{term "st_set(A)"} makes the definition slightly
-         stronger than the HOL one\<close>
-
-  unless_def:    "A unless B == (A - B) co (A \<union> B)"
-
-
 text\<open>SKIP\<close>
 lemma SKIP_in_program [iff,TC]: "SKIP \<in> program"
 by (force simp add: SKIP_def program_def mk_program_def)