equal
deleted
inserted
replaced
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 = "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 = |
27 Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t |
27 Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t |
28 |
28 |