# HG changeset patch
# User huffman
# Date 1117834577 -7200
# Node ID 96f0c85462651a35bf08b3a94cca8c44737f3c61
# Parent  279ab2e02089555be007a31e018969fdcdaf1037
renamed defined lemmas

diff -r 279ab2e02089 -r 96f0c8546265 src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Fri Jun 03 23:35:18 2005 +0200
+++ b/src/HOLCF/Domain.thy	Fri Jun 03 23:36:17 2005 +0200
@@ -98,7 +98,7 @@
   apply (rule_tac p=y in sprodE)
    apply simp
   apply fast
- apply (force intro!: defined_spair)
+ apply (force intro!: spair_defined)
 done
 
 lemma ex_sprod_up_defined_iff:
@@ -110,7 +110,7 @@
   apply (rule_tac p=x in upE1)
    apply simp
   apply fast
- apply (force intro!: defined_spair)
+ apply (force intro!: spair_defined)
 done
 
 lemma ex_ssum_defined_iff:
@@ -125,8 +125,8 @@
    apply (rule disjI1, fast)
   apply (rule disjI2, fast)
  apply (erule disjE)
-  apply (force intro: defined_sinl)
- apply (force intro: defined_sinr)
+  apply (force intro: sinl_defined)
+ apply (force intro: sinr_defined)
 done
 
 lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)"