# HG changeset patch
# User krauss
# Date 1287870124 -7200
# Node ID dbab949c2717d23192cc078c2b0e048fdf54873c
# Parent  374f3ef9f94055feb6098ac373835872e240aa40
integrated partial_function into HOL-Plain

diff -r 374f3ef9f940 -r dbab949c2717 src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Sat Oct 23 23:41:19 2010 +0200
+++ b/src/HOL/FunDef.thy	Sat Oct 23 23:42:04 2010 +0200
@@ -5,11 +5,10 @@
 header {* Function Definitions and Termination Proofs *}
 
 theory FunDef
-imports Wellfounded
+imports Partial_Function Wellfounded
 uses
   "Tools/prop_logic.ML"
   "Tools/sat_solver.ML"
-  ("Tools/Function/function_lib.ML")
   ("Tools/Function/function_common.ML")
   ("Tools/Function/context_tree.ML")
   ("Tools/Function/function_core.ML")
@@ -101,7 +100,6 @@
   "wf R \<Longrightarrow> wfP (in_rel R)"
   by (simp add: wfP_def)
 
-use "Tools/Function/function_lib.ML"
 use "Tools/Function/function_common.ML"
 use "Tools/Function/context_tree.ML"
 use "Tools/Function/function_core.ML"
diff -r 374f3ef9f940 -r dbab949c2717 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sat Oct 23 23:41:19 2010 +0200
+++ b/src/HOL/IsaMakefile	Sat Oct 23 23:42:04 2010 +0200
@@ -145,6 +145,7 @@
 
 PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \
   Complete_Lattice.thy \
+  Complete_Partial_Order.thy \
   Datatype.thy \
   Extraction.thy \
   Fields.thy \
@@ -159,6 +160,7 @@
   Nat.thy \
   Option.thy \
   Orderings.thy \
+  Partial_Function.thy \
   Plain.thy \
   Power.thy \
   Predicate.thy \
@@ -190,6 +192,7 @@
   Tools/Function/lexicographic_order.ML \
   Tools/Function/measure_functions.ML \
   Tools/Function/mutual.ML \
+  Tools/Function/partial_function.ML \
   Tools/Function/pat_completeness.ML \
   Tools/Function/pattern_split.ML \
   Tools/Function/relation.ML \