src/HOL/Import/ImportRecorder.thy
author krauss
Tue, 07 Nov 2006 09:33:47 +0100
changeset 21199 2d83f93c3580
parent 20594 b80c4a5cd018
permissions -rw-r--r--
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0. Richer structures do not inherit from semiring_0 anymore, because anihilation is a theorem there, not an axiom. * Generalized axclass "recpower" to arbitrary monoid, not just commutative semirings.

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