isabelle: src/HOL/Import/HOL/divides.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	const_maps
23686 9d5671f61b31 constant dvd now in class target haftmann parents: 21416 diff changeset	6	"divides" > Divides.times_class.dvd :: "nat => nat => bool"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	7
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	8	thm_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	9	"divides_def" > "HOL4Compat.divides_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	10	"ONE_DIVIDES_ALL" > "HOL4Base.divides.ONE_DIVIDES_ALL"
17188 a26a4fc323ed Updated import. obua parents: 14516 diff changeset	11	"NOT_LT_DIV" > "NatSimprocs.nat_dvd_not_less"
35050 9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields haftmann parents: 33657 diff changeset	12	"DIVIDES_TRANS" > "Rings.dvd_trans"
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields haftmann parents: 33657 diff changeset	13	"DIVIDES_SUB" > "Rings.dvd_diff"
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields haftmann parents: 33657 diff changeset	14	"DIVIDES_REFL" > "Rings.dvd_refl"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	15	"DIVIDES_MULT_LEFT" > "HOL4Base.divides.DIVIDES_MULT_LEFT"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	16	"DIVIDES_MULT" > "Divides.dvd_mult2"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	17	"DIVIDES_LE" > "Divides.dvd_imp_le"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	18	"DIVIDES_FACT" > "HOL4Base.divides.DIVIDES_FACT"
33657 a4179bf442d1 renamed lemmas "anti_sym" -> "antisym" nipkow parents: 27651 diff changeset	19	"DIVIDES_ANTISYM" > "Divides.dvd_antisym"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	20	"DIVIDES_ADD_2" > "HOL4Base.divides.DIVIDES_ADD_2"
35050 9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields haftmann parents: 33657 diff changeset	21	"DIVIDES_ADD_1" > "Rings.dvd_add"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	22	"ALL_DIVIDES_0" > "Divides.dvd_0_right"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	23
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	24	end

author	wenzelm
	Thu, 27 May 2010 18:10:37 +0200
changeset 37146	f652333bbf8e
parent 35050	9f841f20dca6
child 44763	b50d5d694838
permissions	-rw-r--r--