src/HOL/ROOT.ML
author bulwahn
Sat Oct 24 16:55:42 2009 +0200 (2009-10-24)
changeset 33113 0f6e30b87cf1
parent 30126 332e739b6b0e
permissions -rw-r--r--
processing of tuples in introduction rules
wenzelm@29304
     1
(* Classical Higher-order Logic -- batteries included *)
clasohm@923
     2
bulwahn@33113
     3
Toplevel.debug := true;
haftmann@29005
     4
use_thy "Complex_Main";
wenzelm@28263
     5
wenzelm@28263
     6
val HOL_proofs = ! Proofterm.proofs;