isabelle: src/HOL/Import/Generate-HOLLight/GenHOLLight.thy@bf19cc5a7899 (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
19064 bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	8	;skip_import_dir "/home/obua/tmp/cache"
bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	9
bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	10	;skip_import on
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
19064 bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	33	DEF_INR;
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	34
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	35	type_maps
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	36	ind > Nat.ind
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	37	bool > bool
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	38	fun > fun
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	39	N_1 > Product_Type.unit
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	40	prod > "*"
19064 bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	41	num > nat
bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	42	sum > "+";
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	43
17444 a389e5892691 1) mapped .. and == constants obua parents: 17440 diff changeset	44	const_renames
a389e5892691 1) mapped .. and == constants obua parents: 17440 diff changeset	45	"==" > "eqeq"
17490 ec62f340e811 maybe the last bug fix (sigh)? obua parents: 17444 diff changeset	46	".." > "dotdot"
ec62f340e811 maybe the last bug fix (sigh)? obua parents: 17444 diff changeset	47	"ALL" > ALL_list;
17444 a389e5892691 1) mapped .. and == constants obua parents: 17440 diff changeset	48
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	49	const_maps
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	50	T > True
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	51	F > False
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	52	ONE_ONE > HOL4Setup.ONE_ONE
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	53	ONTO > Fun.surj
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	54	"=" > "op ="
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	55	"==>" > "op -->"
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	56	"/\\" > "op &"
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	57	"\\/" > "op \|"
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	58	"!" > All
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	59	"?" > Ex
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	60	"?!" > Ex1
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	61	"~" > Not
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	62	o > Fun.comp
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	63	"@" > "Hilbert_Choice.Eps"
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	64	I > Fun.id
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	65	one > Product_Type.Unity
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	66	LET > HOL4Compat.LET
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	67	mk_pair > Product_Type.Pair_Rep
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	68	"," > Pair
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	69	REP_prod > Rep_Prod
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	70	ABS_prod > Abs_Prod
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	71	FST > fst
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	72	SND > snd
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	73	"_0" > 0 :: nat
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	74	SUC > Suc
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	75	PRE > HOLLightCompat.Pred
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	76	NUMERAL > HOL4Compat.NUMERAL
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	77	"+" > "op +" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	78	"" > "op " :: "nat \<Rightarrow> nat \<Rightarrow> nat"
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	79	"-" > "op -" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	80	BIT0 > HOLLightCompat.NUMERAL_BIT0
19064 bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	81	BIT1 > HOL4Compat.NUMERAL_BIT1
bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	82	INL > Sum_Type.Inl
bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	83	INR > Sum_Type.Inr;
bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	84	(* HAS_SIZE > HOLLightCompat.HAS_SIZE; *)
17440 df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	85
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	86	(*import_until "TYDEF_sum"
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	87
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	88	consts
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	89	print_theorems
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	90
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	91	import_until *)
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	92
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	93	end_import;
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	94
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	95	append_dump "end";
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	96
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	97	flush_dump;
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	98
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	99	import_segment "";
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	100
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	101	end

author	obua
	Wed, 15 Feb 2006 23:57:06 +0100
changeset 19064	bf19cc5a7899
parent 17644	bd59bfd4bf37
child 19203	778507520684
permissions	-rw-r--r--