/src/HOL/Tools/Function/
drwxr-xr-x [up]
-rw-r--r-- 2013-12-07 20:09 +0100 9145 context_tree.ML
-rw-r--r-- 2013-12-07 20:09 +0100 5701 fun.ML
-rw-r--r-- 2013-12-07 20:09 +0100 2183 fun_cases.ML
-rw-r--r-- 2013-12-07 20:09 +0100 11399 function.ML
-rw-r--r-- 2013-12-07 20:09 +0100 14002 function_common.ML
-rw-r--r-- 2013-12-07 20:09 +0100 32019 function_core.ML
-rw-r--r-- 2013-12-07 20:09 +0100 6095 function_elims.ML
-rw-r--r-- 2013-12-07 20:09 +0100 4283 function_lib.ML
-rw-r--r-- 2013-12-07 20:09 +0100 13836 induction_schema.ML
-rw-r--r-- 2013-12-07 20:09 +0100 7155 lexicographic_order.ML
-rw-r--r-- 2013-12-07 20:09 +0100 1915 measure_functions.ML
-rw-r--r-- 2013-12-07 20:09 +0100 10577 mutual.ML
-rw-r--r-- 2013-12-07 20:09 +0100 11991 partial_function.ML
-rw-r--r-- 2013-12-07 20:09 +0100 4971 pat_completeness.ML
-rw-r--r-- 2013-12-07 20:09 +0100 2982 pattern_split.ML
-rw-r--r-- 2013-12-07 20:09 +0100 1429 relation.ML
-rw-r--r-- 2013-12-07 20:09 +0100 11389 scnp_reconstruct.ML
-rw-r--r-- 2013-12-07 20:09 +0100 8469 scnp_solve.ML
-rw-r--r-- 2013-12-07 20:09 +0100 9594 size.ML
-rw-r--r-- 2013-12-07 20:09 +0100 2127 sum_tree.ML
-rw-r--r-- 2013-12-07 20:09 +0100 10922 termination.ML