# HG changeset patch
# User wenzelm
# Date 939667418 -7200
# Node ID 77bac5d8416227e957c43efb6c58fb73acf40dfe
# Parent  2a13c396201df64b84c0b2e2c35fe3d02cc1efed
bind_thm "ccontr";

diff -r 2a13c396201d -r 77bac5d84162 src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Mon Oct 11 20:42:06 1999 +0200
+++ b/src/HOL/HOL_lemmas.ML	Mon Oct 11 20:43:38 1999 +0200
@@ -264,7 +264,7 @@
     rtac (impI RS prem RS eqTrueI) 1,
     etac subst 1,  assume_tac 1]);
 
-val ccontr = FalseE RS classical;
+bind_thm ("ccontr", FalseE RS classical);
 
 (*Double negation law*)
 Goal "~~P ==> P";