Mercurial Mercurial > repos > isabelle / diff
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/Product_Type.thy
changeset 20415 e3d2d7b01279
parent 20380 14f9f2a1caa6
child 20588 c847c56edf0c 
--- a/src/HOL/Product_Type.thy	Fri Aug 25 18:44:59 2006 +0200
+++ b/src/HOL/Product_Type.thy	Fri Aug 25 18:45:57 2006 +0200
@@ -541,7 +541,8 @@
    b) can lead to nontermination in the presence of split_def
 *)
 lemma split_comp_eq: 
-"(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
+  fixes f :: "'a => 'b => 'c" and g :: "'d => 'a"
+  shows "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
   by (rule ext) auto
 
 lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)"
isabelle