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

author	haftmann
	Fri, 12 Oct 2007 08:25:48 +0200
changeset 24996	ebd5f4cc7118
parent 23881	851c74f1bb69
child 34974	18b41bba42b5
permissions	-rw-r--r--