src/HOL/ROOT.ML
author huffman
Tue, 17 Apr 2012 11:03:08 +0200
changeset 47503 cb44d09d9d22
parent 37694 19e8b730ddeb
permissions -rw-r--r--
add theory data for relator identity rules; preprocess transfer rules generated by lift_definition using relator rules


(* Classical Higher-order Logic *)

use_thys ["Complex_Main"];