Mercurial Mercurial > hg > nominal2 / 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.
QuotScript.thy
changeset 166 3300260b63a1
parent 162 20f0b148cfe2
child 171 13aab4c59096
equal deleted inserted replaced
164:4f00ca4f5ef4 166:3300260b63a1 
   496 lemma FORALL_PRS:
 
   496 lemma FORALL_PRS:
 
   497   assumes a: "QUOTIENT R absf repf"
 
   497   assumes a: "QUOTIENT R absf repf"
 
   498   shows "!f. All f = Ball (Respects R) ((absf ---> id) f)"
 
   498   shows "!f. All f = Ball (Respects R) ((absf ---> id) f)"
 
   499   sorry
 
   499   sorry
 
   500 
   500 
       
   501 lemma ho_all_prs: "op = ===> op = ===> op = All All"
 
       
   502   apply (auto)
 
       
   503   done
 
   501 
   504 
   502 end
 
   505 end
 
   503 
   506
nominal2