isabelle: src/HOL/Import/Generate-HOLLight/GenHOLLight.thy@e46e7a9cb622 (annotated)

17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	1	(* Title: HOL/Import/Generate-HOLLight/GenHOLLight.thy
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	2	ID: $Id$
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	3	Author: Steven Obua (TU Muenchen)
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	4	*)
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	5
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	6	theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin;
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	7
20275 f82435d180ef removed skip obua parents: 19233 diff changeset	8	(*;skip_import_dir "/home/obua/tmp/cache"
19064 bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	9
20275 f82435d180ef removed skip obua parents: 19233 diff changeset	10	;skip_import on*)
19064 bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	11
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	12	;import_segment "hollight";
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	13
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	14	setup_dump "../HOLLight" "HOLLight";
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	15
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	16	append_dump {theory HOLLight = "../HOLLightCompat" + "../HOL4Syntax":};
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	17
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	18	;import_theory hollight;
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	19
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	20	ignore_thms
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	21	TYDEF_1
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	22	DEF_one
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	23	TYDEF_prod
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	24	TYDEF_num
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	25	IND_SUC_0_EXISTS
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	26	DEF__0
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	27	DEF_SUC
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	28	DEF_IND_SUC
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	29	DEF_IND_0
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	30	DEF_NUM_REP
19064 bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	31	TYDEF_sum
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	32	DEF_INL
19203 778507520684 Added HOL-ZF to Isabelle. obua parents: 19064 diff changeset	33	DEF_INR
20326 cbf31171c147 fixed generator obua parents: 20275 diff changeset	34	(* TYDEF_option*);
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	35
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	36	type_maps
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	37	ind > Nat.ind
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	38	bool > bool
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	39	fun > fun
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	40	N_1 > Product_Type.unit
37678 0040bafffdef "prod" and "sum" replace "" and "+" respectively haftmann* parents: 37391 diff changeset	41	prod > Product_Type.prod
37391 476270a6c2dc tuned quotes, antiquotations and whitespace haftmann parents: 35267 diff changeset	42	num > Nat.nat
37678 0040bafffdef "prod" and "sum" replace "" and "+" respectively haftmann* parents: 37391 diff changeset	43	sum > Sum_Type.sum
20326 cbf31171c147 fixed generator obua parents: 20275 diff changeset	44	(* option > Datatype.option*);
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	45
17444 a389e5892691 1) mapped .. and == constants obua parents: 17440 diff changeset	46	const_renames
a389e5892691 1) mapped .. and == constants obua parents: 17440 diff changeset	47	"==" > "eqeq"
17490 ec62f340e811 maybe the last bug fix (sigh)? obua parents: 17444 diff changeset	48	".." > "dotdot"
ec62f340e811 maybe the last bug fix (sigh)? obua parents: 17444 diff changeset	49	"ALL" > ALL_list;
17444 a389e5892691 1) mapped .. and == constants obua parents: 17440 diff changeset	50
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	51	const_maps
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	52	T > True
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	53	F > False
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	54	ONE_ONE > HOL4Setup.ONE_ONE
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	55	ONTO > Fun.surj
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	56	"=" > "op ="
38786 e46e7a9cb622 formerly unnamed infix impliciation now named HOL.implies haftmann parents: 37678 diff changeset	57	"==>" > HOL.implies
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	58	"/\\" > "op &"
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	59	"\\/" > "op \|"
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	60	"!" > All
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	61	"?" > Ex
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	62	"?!" > Ex1
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	63	"~" > Not
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	64	o > Fun.comp
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	65	"@" > "Hilbert_Choice.Eps"
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	66	I > Fun.id
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	67	one > Product_Type.Unity
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	68	LET > HOL4Compat.LET
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	69	mk_pair > Product_Type.Pair_Rep
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	70	"," > Pair
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	71	REP_prod > Rep_Prod
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	72	ABS_prod > Abs_Prod
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	73	FST > fst
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	74	SND > snd
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	75	"_0" > 0 :: nat
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	76	SUC > Suc
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	77	PRE > HOLLightCompat.Pred
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	78	NUMERAL > HOL4Compat.NUMERAL
35267 8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy haftmann parents: 34974 diff changeset	79	"+" > Groups.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy haftmann parents: 34974 diff changeset	80	"*" > Groups.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy haftmann parents: 34974 diff changeset	81	"-" > Groups.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	82	BIT0 > HOLLightCompat.NUMERAL_BIT0
19064 bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	83	BIT1 > HOL4Compat.NUMERAL_BIT1
bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	84	INL > Sum_Type.Inl
20326 cbf31171c147 fixed generator obua parents: 20275 diff changeset	85	INR > Sum_Type.Inr
cbf31171c147 fixed generator obua parents: 20275 diff changeset	86	(* NONE > Datatype.None
cbf31171c147 fixed generator obua parents: 20275 diff changeset	87	SOME > Datatype.Some;
cbf31171c147 fixed generator obua parents: 20275 diff changeset	88	HAS_SIZE > HOLLightCompat.HAS_SIZE; *)
17440 df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	89
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	90	(*import_until "TYDEF_sum"
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	91
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	92	consts
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	93	print_theorems
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	94
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	95	import_until *)
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	96
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	97	end_import;
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	98
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	99	append_dump "end";
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	100
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	101	flush_dump;
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	102
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	103	import_segment "";
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	104
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	105	end

author	haftmann
	Thu, 26 Aug 2010 20:51:17 +0200
changeset 38786	e46e7a9cb622
parent 37678	0040bafffdef
child 38795	848be46708dc
permissions	-rw-r--r--