--- 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"
--- 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 \