changeset 29986 | 05354c653d3a |
parent 29950 | 1e0b8e561cc2 |
child 30000 | e7723cb4b2a6 |
1.1 --- a/src/HOL/HOL.thy Fri Feb 20 21:29:34 2009 +0100 1.2 +++ b/src/HOL/HOL.thy Sun Feb 22 10:22:29 2009 +0100 1.3 @@ -28,6 +28,7 @@ 1.4 ("~~/src/Tools/induct_tacs.ML") 1.5 "~~/src/Tools/value.ML" 1.6 "~~/src/Tools/code/code_name.ML" 1.7 + "~~/src/Tools/code/code_wellsorted.ML" (* formal dependency *) 1.8 "~~/src/Tools/code/code_funcgr.ML" 1.9 "~~/src/Tools/code/code_thingol.ML" 1.10 "~~/src/Tools/code/code_printer.ML"