/src/HOL/Tools/Function/
drwxr-xr-x [up]
-rw-r--r-- 2011-01-08 09:34 -0800 8896 context_tree.ML
-rw-r--r-- 2011-01-08 09:34 -0800 5123 fun.ML
-rw-r--r-- 2011-01-08 09:34 -0800 10905 function.ML
-rw-r--r-- 2011-01-08 09:34 -0800 11348 function_common.ML
-rw-r--r-- 2011-01-08 09:34 -0800 33855 function_core.ML
-rw-r--r-- 2011-01-08 09:34 -0800 5229 function_lib.ML
-rw-r--r-- 2011-01-08 09:34 -0800 13854 induction_schema.ML
-rw-r--r-- 2011-01-08 09:34 -0800 7389 lexicographic_order.ML
-rw-r--r-- 2011-01-08 09:34 -0800 1905 measure_functions.ML
-rw-r--r-- 2011-01-08 09:34 -0800 9336 mutual.ML
-rw-r--r-- 2011-01-08 09:34 -0800 7974 partial_function.ML
-rw-r--r-- 2011-01-08 09:34 -0800 5247 pat_completeness.ML
-rw-r--r-- 2011-01-08 09:34 -0800 3091 pattern_split.ML
-rw-r--r-- 2011-01-08 09:34 -0800 1577 relation.ML
-rw-r--r-- 2011-01-08 09:34 -0800 11440 scnp_reconstruct.ML
-rw-r--r-- 2011-01-08 09:34 -0800 8461 scnp_solve.ML
-rw-r--r-- 2011-01-08 09:34 -0800 9641 size.ML
-rw-r--r-- 2011-01-08 09:34 -0800 1663 sum_tree.ML
-rw-r--r-- 2011-01-08 09:34 -0800 10813 termination.ML