isabelle: src/HOL/Import/HOL/powser.imp@f652333bbf8e (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
	Thu, 27 May 2010 18:10:37 +0200
changeset 37146	f652333bbf8e
parent 14516	a183dec876ab
permissions	-rw-r--r--