equal
deleted
inserted
replaced
30 |
30 |
31 (* slots for plugging in arithmetic facts and tactics *) |
31 (* slots for plugging in arithmetic facts and tactics *) |
32 |
32 |
33 structure Arith_Facts = Named_Thms |
33 structure Arith_Facts = Named_Thms |
34 ( |
34 ( |
35 val name = "arith" |
35 val name = @{binding arith} |
36 val description = "arith facts - only ground formulas" |
36 val description = "arith facts -- only ground formulas" |
37 ); |
37 ); |
38 |
38 |
39 val get_arith_facts = Arith_Facts.get; |
39 val get_arith_facts = Arith_Facts.get; |
40 |
40 |
41 structure Arith_Tactics = Theory_Data |
41 structure Arith_Tactics = Theory_Data |