equal
deleted
inserted
replaced
51 val lookup_mode = Symtab.lookup o Modes.get o Context.Proof; |
51 val lookup_mode = Symtab.lookup o Modes.get o Context.Proof; |
52 |
52 |
53 |
53 |
54 structure Mono_Rules = Named_Thms |
54 structure Mono_Rules = Named_Thms |
55 ( |
55 ( |
56 val name = "partial_function_mono"; |
56 val name = @{binding partial_function_mono}; |
57 val description = "monotonicity rules for partial function definitions"; |
57 val description = "monotonicity rules for partial function definitions"; |
58 ); |
58 ); |
59 |
59 |
60 |
60 |
61 (*** Automated monotonicity proofs ***) |
61 (*** Automated monotonicity proofs ***) |