Added ML bindings for sup_fun_eq and sup_bool_eq.
authorberghofe
Wed, 11 Jul 2007 11:02:07 +0200
changeset 23738 3a801ffdc58c
parent 23737 9194aecbf20e
child 23739 c5ead5df7f35
Added ML bindings for sup_fun_eq and sup_bool_eq.
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