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.
Removed needless parentheses from translation
authorpaulson
Fri, 18 Apr 1997 11:48:16 +0200
changeset 2983 f914a1663b2a
parent 2982 85c81d524655
child 2984 b1a5455f0332
Removed needless parentheses from translation
src/HOL/Sum.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Sum.thy	Fri Apr 18 11:47:36 1997 +0200
+++ b/src/HOL/Sum.thy	Fri Apr 18 11:48:16 1997 +0200
@@ -34,7 +34,7 @@
   Part          :: ['a set, 'b => 'a] => 'a set
 
 translations
-  "case p of Inl(x) => a | Inr(y) => b" == "sum_case (%x.a) (%y.b) p"
+  "case p of Inl x => a | Inr y => b" == "sum_case (%x.a) (%y.b) p"
 
 defs
   Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
isabelle