| changeset 32861 | 105f40051387 |
| parent 31299 | 0c5baf034d0e |
| child 33038 | 8f9594c31de4 |
--- a/src/Tools/intuitionistic.ML Fri Oct 02 22:02:54 2009 +0200 +++ b/src/Tools/intuitionistic.ML Fri Oct 02 22:15:08 2009 +0200 @@ -69,7 +69,6 @@ val introN = "intro"; val elimN = "elim"; val destN = "dest"; -val ruleN = "rule"; fun modifier name kind kind' att = Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME)