equal
deleted
inserted
replaced
16 struct |
16 struct |
17 |
17 |
18 (** User-declared size functions **) |
18 (** User-declared size functions **) |
19 structure Measure_Heuristic_Rules = Named_Thms |
19 structure Measure_Heuristic_Rules = Named_Thms |
20 ( |
20 ( |
21 val name = "measure_function" |
21 val name = @{binding measure_function} |
22 val description = |
22 val description = |
23 "rules that guide the heuristic generation of measure functions" |
23 "rules that guide the heuristic generation of measure functions" |
24 ); |
24 ); |
25 |
25 |
26 fun mk_is_measure t = |
26 fun mk_is_measure t = |