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/Tools/function_package/sum_tools.ML
changeset 22622 25693088396b
parent 21237 b803f9870e97 
--- a/src/HOL/Tools/function_package/sum_tools.ML	Tue Apr 10 11:55:23 2007 +0200
+++ b/src/HOL/Tools/function_package/sum_tools.ML	Tue Apr 10 14:11:01 2007 +0200
@@ -31,12 +31,12 @@
 
 val inlN = "Sum_Type.Inl"
 val inrN = "Sum_Type.Inr"
-val sumcaseN = "Datatype.sum.sum_case"
+val sumcaseN = "Sum_Type.sum_case"
 
-val projlN = "FunDef.lproj"
-val projrN = "FunDef.rproj"
-val projl_inl = thm "FunDef.lproj_inl"
-val projr_inr = thm "FunDef.rproj_inr"
+val projlN = "Sum_Type.Projl"
+val projrN = "Sum_Type.Projr"
+val projl_inl = thm "Sum_Type.Projl_Inl"
+val projr_inr = thm "Sum_Type.Projr_Inr"
 
 fun mk_sumT LT RT = Type ("+", [LT, RT])
 fun mk_sumcase TL TR T l r = Const (sumcaseN, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
isabelle