isabelle: src/HOL/Import/HOL/powser.imp@bd49e10bbd24 (annotated)

14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	1	import
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	2
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	3	import_segment "hol4"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	4
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	5	def_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	6	"diffs" > "diffs_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	7
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	8	const_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	9	"diffs" > "HOL4Real.powser.diffs"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	10
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	11	thm_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	12	"diffs_def" > "HOL4Real.powser.diffs_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	13	"diffs" > "HOL4Real.powser.diffs"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	14	"TERMDIFF_LEMMA5" > "HOL4Real.powser.TERMDIFF_LEMMA5"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	15	"TERMDIFF_LEMMA4" > "HOL4Real.powser.TERMDIFF_LEMMA4"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	16	"TERMDIFF_LEMMA3" > "HOL4Real.powser.TERMDIFF_LEMMA3"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	17	"TERMDIFF_LEMMA2" > "HOL4Real.powser.TERMDIFF_LEMMA2"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	18	"TERMDIFF_LEMMA1" > "HOL4Real.powser.TERMDIFF_LEMMA1"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	19	"TERMDIFF" > "HOL4Real.powser.TERMDIFF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	20	"POWSER_INSIDEA" > "HOL4Real.powser.POWSER_INSIDEA"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	21	"POWSER_INSIDE" > "HOL4Real.powser.POWSER_INSIDE"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	22	"POWREV" > "HOL4Real.powser.POWREV"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	23	"POWDIFF_LEMMA" > "HOL4Real.powser.POWDIFF_LEMMA"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	24	"POWDIFF" > "HOL4Real.powser.POWDIFF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	25	"DIFFS_NEG" > "HOL4Real.powser.DIFFS_NEG"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	26	"DIFFS_LEMMA2" > "HOL4Real.powser.DIFFS_LEMMA2"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	27	"DIFFS_LEMMA" > "HOL4Real.powser.DIFFS_LEMMA"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	28	"DIFFS_EQUIV" > "HOL4Real.powser.DIFFS_EQUIV"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	29
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	30	end

author	wenzelm
	Tue, 06 Sep 2005 18:49:25 +0200
changeset 17287	bd49e10bbd24
parent 14516	a183dec876ab
permissions	-rw-r--r--