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.
explicit type variables prevent empty sorts
authorpaulson
Fri, 25 Aug 2006 18:45:57 +0200
changeset 20415 e3d2d7b01279
parent 20414 029c4f9dc6f4
child 20416 f9cb300118ca
explicit type variables prevent empty sorts
src/HOL/Product_Type.thy file | annotate | diff | comparison | revisions 
--- 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