# HG changeset patch
# User clasohm
# Date 826585162 -3600
# Node ID fd1b9c721ac714e1fd5fec16664ca3db28b1a8d0
# Parent  a89f246dee0eef01e94044e3ae2c6415b4dd0e5b
added constdefs section

diff -r a89f246dee0e -r fd1b9c721ac7 src/HOL/IOA/ABP/Correctness.ML
--- a/src/HOL/IOA/ABP/Correctness.ML	Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/IOA/ABP/Correctness.ML	Mon Mar 11 23:59:22 1996 +0100
@@ -393,8 +393,9 @@
 
 by (simp_tac (impl_ss delsimps ([srch_ioa_def, rsch_ioa_def, srch_fin_ioa_def,
                                  rsch_fin_ioa_def] @ env_ioas @ impl_ioas)
-                      addsimps [system_def, system_fin_def, abs_def, impl_def,
-                                impl_fin_def, sys_IOA, sys_fin_IOA]) 1);
+                      addsimps [system_def, system_fin_def, abs_def,
+                                impl_ioa_def, impl_fin_ioa_def, sys_IOA,
+                                sys_fin_IOA]) 1);
 
 by (REPEAT (EVERY[rtac fxg_is_weak_pmap_of_product_IOA 1, 
                   simp_tac (ss addsimps abstractions) 1,
diff -r a89f246dee0e -r fd1b9c721ac7 src/HOL/IOA/ABP/Impl.thy
--- a/src/HOL/IOA/ABP/Impl.thy	Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/IOA/ABP/Impl.thy	Mon Mar 11 23:59:22 1996 +0100
@@ -15,21 +15,21 @@
 (*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)
 
 
-consts
+constdefs
+
  impl_ioa    :: ('m action, 'm impl_state)ioa
+ "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
+
  sen         :: 'm impl_state => 'm sender_state
- rec         :: 'm impl_state => 'm receiver_state
- srch        :: 'm impl_state => 'm packet list
- rsch        :: 'm impl_state => bool list
+ "sen == fst"
 
-defs
-
- impl_def
-  "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
+ rec         :: 'm impl_state => 'm receiver_state
+ "rec == fst o snd"
 
- sen_def   "sen == fst"
- rec_def   "rec == fst o snd"
- srch_def "srch == fst o snd o snd"
- rsch_def "rsch == snd o snd o snd"
+ srch        :: 'm impl_state => 'm packet list
+ "srch == fst o snd o snd"
+
+ rsch        :: 'm impl_state => bool list
+ "rsch == snd o snd o snd"
 
 end
diff -r a89f246dee0e -r fd1b9c721ac7 src/HOL/IOA/ABP/Impl_finite.thy
--- a/src/HOL/IOA/ABP/Impl_finite.thy	Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/IOA/ABP/Impl_finite.thy	Mon Mar 11 23:59:22 1996 +0100
@@ -14,22 +14,23 @@
 = "'m sender_state * 'm receiver_state * 'm packet list * bool list"
 (*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)
 
-consts
+constdefs
 
  impl_fin_ioa    :: ('m action, 'm impl_fin_state)ioa
+ "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa ||
+                   rsch_fin_ioa)"
+
  sen_fin         :: 'm impl_fin_state => 'm sender_state
- rec_fin         :: 'm impl_fin_state => 'm receiver_state
- srch_fin        :: 'm impl_fin_state => 'm packet list
- rsch_fin        :: 'm impl_fin_state => bool list
-
-defs
+ "sen_fin == fst"
 
- impl_fin_def
-  "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa || rsch_fin_ioa)"
- sen_fin_def   "sen_fin == fst"
- rec_fin_def   "rec_fin == fst o snd"
- srch_fin_def "srch_fin == fst o snd o snd"
- rsch_fin_def "rsch_fin == snd o snd o snd"
+ rec_fin         :: 'm impl_fin_state => 'm receiver_state
+ "rec_fin == fst o snd"
+
+ srch_fin        :: 'm impl_fin_state => 'm packet list
+ "srch_fin == fst o snd o snd"
+
+ rsch_fin        :: 'm impl_fin_state => bool list
+ "rsch_fin == snd o snd o snd"
 
 end
 
diff -r a89f246dee0e -r fd1b9c721ac7 src/HOL/IOA/ABP/Packet.thy
--- a/src/HOL/IOA/ABP/Packet.thy	Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/IOA/ABP/Packet.thy	Mon Mar 11 23:59:22 1996 +0100
@@ -12,14 +12,12 @@
 
    'msg packet = "bool * 'msg"
 
-consts
+constdefs
 
   hdr  :: 'msg packet => bool
-  msg :: 'msg packet => 'msg
+  "hdr == fst"
 
-defs
-
-  hdr_def "hdr == fst"
-  msg_def "msg == snd"
+  msg :: 'msg packet => 'msg
+  "msg == snd"
 
 end
diff -r a89f246dee0e -r fd1b9c721ac7 src/HOL/IOA/NTP/Correctness.thy
--- a/src/HOL/IOA/NTP/Correctness.thy	Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/IOA/NTP/Correctness.thy	Mon Mar 11 23:59:22 1996 +0100
@@ -8,14 +8,10 @@
 
 Correctness = Solve + Impl + Spec +
 
-consts
-
-hom :: 'm impl_state => 'm list
+constdefs
 
-defs
-
-hom_def 
-"hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) 
-                        else ttl(sq(sen s)))"
+  hom :: 'm impl_state => 'm list
+  "hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) 
+                          else ttl(sq(sen s)))"
 
 end
diff -r a89f246dee0e -r fd1b9c721ac7 src/HOL/IOA/NTP/Packet.thy
--- a/src/HOL/IOA/NTP/Packet.thy	Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/IOA/NTP/Packet.thy	Mon Mar 11 23:59:22 1996 +0100
@@ -12,14 +12,12 @@
 
    'msg packet = "bool * 'msg"
 
-consts
+constdefs
 
   hdr  :: 'msg packet => bool
-  msg :: 'msg packet => 'msg
+  "hdr == fst"
 
-defs
-
-  hdr_def "hdr == fst"
-  msg_def "msg == snd"
+  msg :: 'msg packet => 'msg
+  "msg == snd"
 
 end
diff -r a89f246dee0e -r fd1b9c721ac7 src/HOL/IOA/meta_theory/Solve.thy
--- a/src/HOL/IOA/meta_theory/Solve.thy	Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/IOA/meta_theory/Solve.thy	Mon Mar 11 23:59:22 1996 +0100
@@ -8,13 +8,9 @@
 
 Solve = IOA +
 
-consts
+constdefs
 
   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 &                      
diff -r a89f246dee0e -r fd1b9c721ac7 src/HOL/ex/Acc.thy
--- a/src/HOL/ex/Acc.thy	Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/ex/Acc.thy	Mon Mar 11 23:59:22 1996 +0100
@@ -11,13 +11,13 @@
 
 Acc = WF + 
 
+constdefs
+  pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)
+  "pred x r == {y. (y,x):r}"
+
 consts
-  pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)
   acc  :: "('a * 'a)set => 'a set"              (*Accessible part*)
 
-defs
-  pred_def  "pred x r == {y. (y,x):r}"
-
 inductive "acc(r)"
   intrs
     pred    "pred a r: Pow(acc(r)) ==> a: acc(r)"