equal
deleted
inserted
replaced
31 "P \<equiv> False \<Longrightarrow> \<not> P" |
31 "P \<equiv> False \<Longrightarrow> \<not> P" |
32 "\<not> P \<Longrightarrow> (P \<equiv> False)" |
32 "\<not> P \<Longrightarrow> (P \<equiv> False)" |
33 by auto |
33 by auto |
34 |
34 |
35 named_theorems algebra "pre-simplification rules for algebraic methods" |
35 named_theorems algebra "pre-simplification rules for algebraic methods" |
36 ML_file "Tools/groebner.ML" |
36 ML_file \<open>Tools/groebner.ML\<close> |
37 |
37 |
38 method_setup algebra = \<open> |
38 method_setup algebra = \<open> |
39 let |
39 let |
40 fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () |
40 fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () |
41 val addN = "add" |
41 val addN = "add" |