# HG changeset patch
# User berghofe
# Date 1184144527 -7200
# Node ID 3a801ffdc58c2d2a58fc3c7bb2c14e365c362ebc
# Parent  9194aecbf20e521cccc232470c1fec9e7f0538b8
Added ML bindings for sup_fun_eq and sup_bool_eq.

diff -r 9194aecbf20e -r 3a801ffdc58c src/HOL/Fun.thy
--- 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