| changeset 7422 | c63d619286a3 |
| parent 7355 | 4c43090659ca |
| child 9264 | 051592f4236a |
--- a/src/FOL/FOL_lemmas1.ML Wed Sep 01 21:21:01 1999 +0200 +++ b/src/FOL/FOL_lemmas1.ML Wed Sep 01 21:21:22 1999 +0200 @@ -7,7 +7,7 @@ *) val classical = thm "classical"; -val ccontr = FalseE RS classical; +bind_thm ("ccontr", FalseE RS classical); (*** Classical introduction rules for | and EX ***)