equal
deleted
inserted
replaced
30 "P \<equiv> False \<Longrightarrow> \<not> P" |
30 "P \<equiv> False \<Longrightarrow> \<not> P" |
31 "\<not> P \<Longrightarrow> (P \<equiv> False)" |
31 "\<not> P \<Longrightarrow> (P \<equiv> False)" |
32 by auto |
32 by auto |
33 |
33 |
34 ML {* |
34 ML {* |
35 structure Algebra_Simplification = Named_Thms( |
35 structure Algebra_Simplification = Named_Thms |
36 val name = "algebra" |
36 ( |
|
37 val name = @{binding algebra} |
37 val description = "pre-simplification rules for algebraic methods" |
38 val description = "pre-simplification rules for algebraic methods" |
38 ) |
39 ) |
39 *} |
40 *} |
40 |
41 |
41 setup Algebra_Simplification.setup |
42 setup Algebra_Simplification.setup |