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/BNF_Def.thy
changeset 61681 ca53150406c9
parent 61424 c3658c18b7bc
child 62324 ae44f16dcea5 
--- a/src/HOL/BNF_Def.thy	Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/BNF_Def.thy	Sun Nov 15 12:39:51 2015 +0100
@@ -24,8 +24,6 @@
   "R1 a c \<Longrightarrow> rel_sum R1 R2 (Inl a) (Inl c)"
 | "R2 b d \<Longrightarrow> rel_sum R1 R2 (Inr b) (Inr d)"
 
-hide_fact rel_sum_def
-
 definition
   rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
 where
isabelle