src/HOL/Import/ImportRecorder.thy
author bulwahn
Mon, 23 Aug 2010 16:47:57 +0200
changeset 38665 e92223c886f8
parent 20594 b80c4a5cd018
permissions -rw-r--r--
introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets

theory ImportRecorder imports Main 
uses  "seq.ML" "scan.ML" "mono_seq.ML" "mono_scan.ML" "lazy_seq.ML" "xml.ML" "xmlconv.ML" "importrecorder.ML"
begin
end