Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOLCF/Fixrec.thy
changeset 41029 f7d8cfa6e7fc
parent 40834 a1249aeff5b6
child 41429 cf5f025bc3c7
equal deleted inserted replaced
41028:0acff85f95c7 41029:f7d8cfa6e7fc 
    34 apply (rule_tac p=x in oneE, simp, simp)
 
    34 apply (rule_tac p=x in oneE, simp, simp)
 
    35 apply (rule_tac p=y in upE, simp, simp add: cont_Abs_match)
 
    35 apply (rule_tac p=y in upE, simp, simp add: cont_Abs_match)
 
    36 done
 
    36 done
 
    37 
    37 
    38 lemma succeed_defined [simp]: "succeed\<cdot>x \<noteq> \<bottom>"
 
    38 lemma succeed_defined [simp]: "succeed\<cdot>x \<noteq> \<bottom>"
 
    39 by (simp add: succeed_def cont_Abs_match Abs_match_defined)
 
    39 by (simp add: succeed_def cont_Abs_match Abs_match_bottom_iff)
 
    40 
    40 
    41 lemma fail_defined [simp]: "fail \<noteq> \<bottom>"
 
    41 lemma fail_defined [simp]: "fail \<noteq> \<bottom>"
 
    42 by (simp add: fail_def Abs_match_defined)
 
    42 by (simp add: fail_def Abs_match_bottom_iff)
 
    43 
    43 
    44 lemma succeed_eq [simp]: "(succeed\<cdot>x = succeed\<cdot>y) = (x = y)"
 
    44 lemma succeed_eq [simp]: "(succeed\<cdot>x = succeed\<cdot>y) = (x = y)"
 
    45 by (simp add: succeed_def cont_Abs_match Abs_match_inject)
 
    45 by (simp add: succeed_def cont_Abs_match Abs_match_inject)
 
    46 
    46 
    47 lemma succeed_neq_fail [simp]:
 
    47 lemma succeed_neq_fail [simp]:
isabelle