author | berghofe |
Wed, 11 Jul 2007 11:02:07 +0200 | |
changeset 23738 | 3a801ffdc58c |
parent 23737 | 9194aecbf20e |
child 23739 | c5ead5df7f35 |
src/HOL/Fun.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Fun.thy Wed Jul 11 11:01:24 2007 +0200 +++ b/src/HOL/Fun.thy Wed Jul 11 11:02:07 2007 +0200 @@ -600,6 +600,8 @@ val datatype_injI = @{thm datatype_injI} val range_ex1_eq = @{thm range_ex1_eq} val expand_fun_eq = @{thm expand_fun_eq} +val sup_fun_eq = @{thm sup_fun_eq} +val sup_bool_eq = @{thm sup_bool_eq} *} end