src/HOL/ROOT.ML
changeset 28263 69eaa97e7e96
parent 27421 7e458bd56860
child 28952 15a4b2cf8c34
     1.1 --- a/src/HOL/ROOT.ML	Wed Sep 17 21:27:08 2008 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Wed Sep 17 21:27:14 2008 +0200
     1.3 @@ -5,3 +5,6 @@
     1.4  *)
     1.5  
     1.6  use_thy "Complex/Complex_Main";
     1.7 +
     1.8 +val HOL_proofs = ! Proofterm.proofs;
     1.9 +