Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
renamed defined lemmas
authorhuffman
Fri, 03 Jun 2005 23:36:17 +0200
changeset 16217 96f0c8546265
parent 16216 279ab2e02089
child 16218 ea49a9c7ff7c
renamed defined lemmas
src/HOLCF/Domain.thy file | annotate | diff | comparison | revisions 
--- 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>)"
isabelle