src/HOL/Tools/Function/function_common.ML
changeset 38764 e6a18808873c
parent 38761 b32975d3db3e
child 39134 917b4b6ba3d2
equal deleted inserted replaced
38763:283f1f9969ba 38764:e6a18808873c
   162 (* Simp rules for termination proofs *)
   162 (* Simp rules for termination proofs *)
   163 
   163 
   164 structure Termination_Simps = Named_Thms
   164 structure Termination_Simps = Named_Thms
   165 (
   165 (
   166   val name = "termination_simp"
   166   val name = "termination_simp"
   167   val description = "Simplification rule for termination proofs"
   167   val description = "simplification rules for termination proofs"
   168 )
   168 )
   169 
   169 
   170 
   170 
   171 (* Default Termination Prover *)
   171 (* Default Termination Prover *)
   172 
   172