author | wenzelm |
Thu, 12 Mar 2009 21:29:04 +0100 | |
changeset 30480 | f3421e8379ab |
parent 30479 | fc58fb1f83ad |
child 30481 | de003023c302 |
--- a/src/HOL/FunDef.thy Thu Mar 12 16:13:14 2009 +0100 +++ b/src/HOL/FunDef.thy Thu Mar 12 21:29:04 2009 +0100 @@ -314,13 +314,11 @@ use "Tools/function_package/scnp_reconstruct.ML" setup {* ScnpReconstruct.setup *} -(* -setup {* + +ML_val -- "setup inactive" +{* Context.theory_map (FundefCommon.set_termination_prover (ScnpReconstruct.decomp_scnp [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])) *} -*) - - end