isabelle: src/HOL/Import/Generate-HOL/GenHOL4Real.thy@043f8dc3b51f (annotated)

14620 1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	1	(* Title: HOL/Import/Generate-HOL/GenHOL4Real.thy
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	2	Author: Sebastian Skalberg (TU Muenchen)
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	3	*)
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	4
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 15647 diff changeset	5	theory GenHOL4Real imports GenHOL4Base begin
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	6
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	7	import_segment "hol4";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	8
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	9	setup_dump "../HOL" "HOL4Real";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	10
17566 484ff733f29c new header syntax; wenzelm parents: 16417 diff changeset	11	append_dump "theory HOL4Real imports HOL4Base begin";
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	12
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	13	import_theory realax;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	14
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	15	type_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	16	real > RealDef.real;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	17
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	18	const_maps
35267 8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy haftmann parents: 35092 diff changeset	19	real_0 > Groups.zero :: real
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy haftmann parents: 35092 diff changeset	20	real_1 > Groups.one :: real
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy haftmann parents: 35092 diff changeset	21	real_neg > Groups.uminus :: "real => real"
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy haftmann parents: 35092 diff changeset	22	inv > Groups.inverse :: "real => real"
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy haftmann parents: 35092 diff changeset	23	real_add > Groups.plus :: "[real,real] => real"
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy haftmann parents: 35092 diff changeset	24	real_mul > Groups.times :: "[real,real] => real"
35092 cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy haftmann parents: 34974 diff changeset	25	real_lt > Orderings.less :: "[real,real] => bool";
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	26
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	27	ignore_thms
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	28	real_TY_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	29	real_tybij
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	30	real_0
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	31	real_1
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	32	real_neg
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	33	real_inv
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	34	real_add
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	35	real_mul
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	36	real_lt
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	37	real_of_hreal
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	38	hreal_of_real
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	39	REAL_ISO_EQ
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	40	REAL_POS
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	41	SUP_ALLPOS_LEMMA1
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	42	SUP_ALLPOS_LEMMA2
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	43	SUP_ALLPOS_LEMMA3
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	44	SUP_ALLPOS_LEMMA4;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	45
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	46	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	47
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	48	import_theory real;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	49
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	50	const_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	51	real_gt > HOL4Compat.real_gt
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	52	real_ge > HOL4Compat.real_ge
35092 cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy haftmann parents: 34974 diff changeset	53	real_lte > Orderings.less_eq :: "[real,real] => bool"
35267 8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy haftmann parents: 35092 diff changeset	54	real_sub > Groups.minus :: "[real,real] => real"
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy haftmann parents: 35092 diff changeset	55	"/" > Rings.divide :: "[real,real] => real"
34974 18b41bba42b5 new theory Algebras.thy for generic algebraic structures haftmann parents: 24996 diff changeset	56	pow > Power.power :: "[real,nat] => real"
35092 cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy haftmann parents: 34974 diff changeset	57	abs > Groups.abs :: "real => real"
15647 b1f486a9c56b Updated import configuration. skalberg parents: 14620 diff changeset	58	real_of_num > RealDef.real :: "nat => real";
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	59
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	60	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	61
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	62	import_theory topology;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	63	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	64
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	65	import_theory nets;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	66	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	67
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	68	import_theory seq;
17694 b7870c2bd7df mapped "-->" to "hol4-->" obua parents: 17566 diff changeset	69	const_renames
b7870c2bd7df mapped "-->" to "hol4-->" obua parents: 17566 diff changeset	70	"-->" > "hol4-->";
b7870c2bd7df mapped "-->" to "hol4-->" obua parents: 17566 diff changeset	71
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	72	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	73
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	74	import_theory lim;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	75	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	76
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	77	import_theory powser;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	78	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	79
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	80	import_theory transc;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	81	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	82
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	83	import_theory poly;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	84	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	85
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	86	append_dump "end";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	87
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	88	flush_dump;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	89
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	90	import_segment "";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	91
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	92	end

author	blanchet
	Wed, 15 Dec 2010 18:10:32 +0100
changeset 41171	043f8dc3b51f
parent 35267	8dfd816713c6
child 44064	5bce8ff0d9ae
permissions	-rw-r--r--