Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/FunDef.thy
changeset 54407 e95831757903
parent 53603 59ef06cda7b9
equal deleted inserted replaced
54406:a2d18fea844a 54407:e95831757903 
   308 ML_file "Tools/Function/termination.ML"
 
   308 ML_file "Tools/Function/termination.ML"
 
   309 ML_file "Tools/Function/scnp_solve.ML"
 
   309 ML_file "Tools/Function/scnp_solve.ML"
 
   310 ML_file "Tools/Function/scnp_reconstruct.ML"
 
   310 ML_file "Tools/Function/scnp_reconstruct.ML"
 
   311 ML_file "Tools/Function/fun_cases.ML"
 
   311 ML_file "Tools/Function/fun_cases.ML"
 
   312 
   312 
   313 setup {* ScnpReconstruct.setup *}
 
   313 setup ScnpReconstruct.setup
 
   314 
   314 
   315 ML_val -- "setup inactive"
 
   315 ML_val -- "setup inactive"
 
   316 {*
 
   316 {*
 
   317   Context.theory_map (Function_Common.set_termination_prover
 
   317   Context.theory_map (Function_Common.set_termination_prover
 
   318     (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))
 
   318     (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))
isabelle