isabelle: src/HOL/Import/Generate-HOLLight/GenHOLLight.thy@b3e7da94b51f (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
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	8	;import_segment "hollight";
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	9
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	10	setup_dump "../HOLLight" "HOLLight";
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	11
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	12	append_dump {theory HOLLight = "../HOLLightCompat" + "../HOL4Syntax":};
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	13
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	14	;import_theory hollight;
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	15
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	16	ignore_thms
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	17	TYDEF_1
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	18	DEF_one
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	19	TYDEF_prod
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	20	TYDEF_num
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	21	IND_SUC_0_EXISTS
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	22	DEF__0
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	23	DEF_SUC
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	24	DEF_IND_SUC
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	25	DEF_IND_0
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	26	DEF_NUM_REP
17440 df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	27	(* TYDEF_sum
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	28	DEF_INL
17440 df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	29	DEF_INR*);
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	30
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	31	type_maps
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	32	ind > Nat.ind
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	33	bool > bool
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	34	fun > fun
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	35	N_1 > Product_Type.unit
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	36	prod > "*"
17440 df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	37	num > nat;
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	38	(* sum > "+";*)
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	39
17444 a389e5892691 1) mapped .. and == constants obua parents: 17440 diff changeset	40	const_renames
a389e5892691 1) mapped .. and == constants obua parents: 17440 diff changeset	41	"==" > "eqeq"
17490 ec62f340e811 maybe the last bug fix (sigh)? obua parents: 17444 diff changeset	42	".." > "dotdot"
ec62f340e811 maybe the last bug fix (sigh)? obua parents: 17444 diff changeset	43	"ALL" > ALL_list;
17444 a389e5892691 1) mapped .. and == constants obua parents: 17440 diff changeset	44
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	45	const_maps
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	46	T > True
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	47	F > False
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	48	ONE_ONE > HOL4Setup.ONE_ONE
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	49	ONTO > Fun.surj
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	50	"=" > "op ="
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	51	"==>" > "op -->"
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	52	"/\\" > "op &"
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	53	"\\/" > "op \|"
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	54	"!" > All
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	55	"?" > Ex
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	56	"?!" > Ex1
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	57	"~" > Not
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	58	o > Fun.comp
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	59	"@" > "Hilbert_Choice.Eps"
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	60	I > Fun.id
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	61	one > Product_Type.Unity
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	62	LET > HOL4Compat.LET
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	63	mk_pair > Product_Type.Pair_Rep
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	64	"," > Pair
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	65	REP_prod > Rep_Prod
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	66	ABS_prod > Abs_Prod
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	67	FST > fst
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	68	SND > snd
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	69	"_0" > 0 :: nat
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	70	SUC > Suc
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	71	PRE > HOLLightCompat.Pred
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	72	NUMERAL > HOL4Compat.NUMERAL
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	73	"+" > "op +" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	74	"" > "op " :: "nat \<Rightarrow> nat \<Rightarrow> nat"
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	75	"-" > "op -" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	76	BIT0 > HOLLightCompat.NUMERAL_BIT0
17440 df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	77	BIT1 > HOL4Compat.NUMERAL_BIT1;
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	78	(* INL > Sum_Type.Inl
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	79	INR > Sum_Type.Inr
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	80	HAS_SIZE > HOLLightCompat.HAS_SIZE*)
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	81
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	82	(*import_until "TYDEF_sum"
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	83
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	84	consts
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	85	print_theorems
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	86
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	87	import_until *)
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	88
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	89	end_import;
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	90
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	91	append_dump "end";
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	92
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	93	flush_dump;
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	94
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	95	import_segment "";
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	96
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	97	end

author	urbanc
	Tue, 13 Dec 2005 18:11:21 +0100
changeset 18396	b3e7da94b51f
parent 17644	bd59bfd4bf37
child 19064	bf19cc5a7899
permissions	-rw-r--r--