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
     1 (* Classical Higher-order Logic -- batteries included *)
     2 
     3 Toplevel.debug := true;
     4 use_thy "Complex_Main";
     5 
     6 val HOL_proofs = ! Proofterm.proofs;