isabelle: src/HOL/Import/HOL_Light/Template/GenHOLLight.thy@ed681ca1188a (annotated)

46879 a8b1236e0837 tuned headers; wenzelm parents: 46796 diff changeset	1	(* Title: HOL/Import/HOL_Light/Template/GenHOLLight.thy
41589 bbd861837ebc tuned headers; wenzelm parents: 38864 diff changeset	2	Author: Steven Obua, TU Muenchen
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	3	Author: Cezary Kaliszyk
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	4	*)
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	5
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	6	theory GenHOLLight
46796 81e5ec0a3cd0 one unified Importer theory haftmann parents: 46787 diff changeset	7	imports "../../Importer" "../Compatibility"
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	8	begin
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	9
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	10	import_segment "hollight"
19064 bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	11
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	12	setup_dump "../Generated" "HOLLight"
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	13
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	14	append_dump {*theory HOL4Base
46796 81e5ec0a3cd0 one unified Importer theory haftmann parents: 46787 diff changeset	15	imports "../../Importer" "../Compatibility"
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	16	begin
3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	17	*}
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	18
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	19	import_theory "~~/src/HOL/Import/HOL_Light/Generated" hollight
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	20
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	21	;ignore_thms
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	22	(* Unit type *)
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	23	TYDEF_1 DEF_one
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	24	(* Product type *)
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	25	TYDEF_prod "DEF_," DEF_mk_pair REP_ABS_PAIR
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	26	(* Option type *)
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	27	TYDEF_option DEF_NONE DEF_SOME
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	28	(* Sum type *)
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	29	TYDEF_sum DEF_INL DEF_INR DEF_OUTL DEF_OUTR
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	30	(* Naturals *)
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	31	TYDEF_num DEF__0 DEF_SUC
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	32	(* Lists *)
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	33	TYDEF_list DEF_NIL DEF_CONS DEF_HD DEF_TL DEF_MAP2 DEF_ITLIST2 ALL_MAP EX_MAP
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	34	DEF_ASSOC MEM_ASSOC DEF_ZIP EL_TL
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	35
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	36	(* list_of_set uses Isabelle lists with HOLLight CARD *)
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	37	DEF_list_of_set LIST_OF_SET_PROPERTIES SET_OF_LIST_OF_SET LENGTH_LIST_OF_SET
43843 16f2fd9103bd HOL/Import: Fix errors with _mk_list Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 43785 diff changeset	38	MEM_LIST_OF_SET HAS_SIZE_SET_OF_LIST FINITE_SET_OF_LIST
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	39	(* UNIV *)
43843 16f2fd9103bd HOL/Import: Fix errors with _mk_list Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 43785 diff changeset	40	DIMINDEX_FINITE_SUM DIMINDEX_HAS_SIZE_FINITE_SUM FSTCART_PASTECART
16f2fd9103bd HOL/Import: Fix errors with _mk_list Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 43785 diff changeset	41	SNDCART_PASTECART PASTECART_FST_SND PASTECART_EQ FORALL_PASTECART EXISTS_PASTECART
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	42	(* Reals *)
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	43	(* TYDEF_real DEF_real_of_num DEF_real_neg DEF_real_add DEF_real_mul DEF_real_le
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	44	DEF_real_inv REAL_HREAL_LEMMA1 REAL_HREAL_LEMMA2 *)
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	45	(* Integers *)
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	46	(* TYDEF_int DEF_int_divides DEF_int_coprime*)
43843 16f2fd9103bd HOL/Import: Fix errors with _mk_list Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 43785 diff changeset	47	(* HOLLight CARD and CASEWISE with Isabelle lists *)
16f2fd9103bd HOL/Import: Fix errors with _mk_list Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 43785 diff changeset	48	CARD_SET_OF_LIST_LE CASEWISE CASEWISE_CASES RECURSION_CASEWISE CASEWISE_WORKS
16f2fd9103bd HOL/Import: Fix errors with _mk_list Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 43785 diff changeset	49	WF_REC_CASES RECURSION_CASEWISE_PAIRWISE
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	50
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	51	;type_maps
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	52	bool > HOL.bool
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	53	"fun" > "fun"
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	54	N_1 > Product_Type.unit
37678 0040bafffdef "prod" and "sum" replace "" and "+" respectively haftmann* parents: 37391 diff changeset	55	prod > Product_Type.prod
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	56	ind > Nat.ind
37391 476270a6c2dc tuned quotes, antiquotations and whitespace haftmann parents: 35267 diff changeset	57	num > Nat.nat
37678 0040bafffdef "prod" and "sum" replace "" and "+" respectively haftmann* parents: 37391 diff changeset	58	sum > Sum_Type.sum
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	59	option > Datatype.option
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	60	list > List.list
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	61	(real > RealDef.real )
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	62	(int > Int.int )
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	63
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	64	;const_renames
17444 a389e5892691 1) mapped .. and == constants obua parents: 17440 diff changeset	65	"==" > "eqeq"
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	66	"ALL" > list_ALL
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	67	"EX" > list_EX
17444 a389e5892691 1) mapped .. and == constants obua parents: 17440 diff changeset	68
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	69	;const_maps
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	70	T > HOL.True
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	71	F > HOL.False
38864 4abe644fcea5 formerly unnamed infix equality now named HOL.eq haftmann parents: 38795 diff changeset	72	"=" > HOL.eq
38786 e46e7a9cb622 formerly unnamed infix impliciation now named HOL.implies haftmann parents: 37678 diff changeset	73	"==>" > HOL.implies
38795 848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj haftmann parents: 38786 diff changeset	74	"/\\" > HOL.conj
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj haftmann parents: 38786 diff changeset	75	"\\/" > HOL.disj
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	76	"!" > HOL.All
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	77	"?" > HOL.Ex
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	78	"?!" > HOL.Ex1
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	79	"~" > HOL.Not
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	80	COND > HOL.If
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	81	ONE_ONE > Fun.inj
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	82	ONTO > Fun.surj
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	83	o > Fun.comp
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	84	"@" > Hilbert_Choice.Eps
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	85	CHOICE > Hilbert_Choice.Eps
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	86	I > Fun.id
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	87	one > Product_Type.Unity
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	88	LET > HOLLightCompat.LET
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	89	mk_pair > Product_Type.Pair_Rep
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	90	"," > Product_Type.Pair
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	91	FST > Product_Type.fst
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	92	SND > Product_Type.snd
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	93	CURRY > Product_Type.curry
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	94	"_0" > Groups.zero_class.zero :: nat
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	95	SUC > Nat.Suc
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	96	PRE > HOLLightCompat.Pred
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	97	NUMERAL > HOLLightCompat.NUMERAL
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	98	mk_num > Fun.id
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	99	"+" > Groups.plus_class.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	100	"*" > Groups.times_class.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	101	"-" > Groups.minus_class.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	102	"<" > Orderings.ord_class.less :: "nat \<Rightarrow> nat \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	103	"<=" > Orderings.ord_class.less_eq :: "nat \<Rightarrow> nat \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	104	">" > Orderings.ord_class.greater :: "nat \<Rightarrow> nat \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	105	">=" > Orderings.ord_class.greater_eq :: "nat \<Rightarrow> nat \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	106	EXP > Power.power_class.power :: "nat \<Rightarrow> nat \<Rightarrow> nat"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	107	MAX > Orderings.ord_class.max :: "nat \<Rightarrow> nat \<Rightarrow> nat"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	108	MIN > Orderings.ord_class.min :: "nat \<Rightarrow> nat \<Rightarrow> nat"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	109	DIV > Divides.div_class.div :: "nat \<Rightarrow> nat \<Rightarrow> nat"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	110	MOD > Divides.div_class.mod :: "nat \<Rightarrow> nat \<Rightarrow> nat"
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	111	BIT0 > HOLLightCompat.NUMERAL_BIT0
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	112	BIT1 > HOLLightCompat.NUMERAL_BIT1
19064 bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	113	INL > Sum_Type.Inl
20326 cbf31171c147 fixed generator obua parents: 20275 diff changeset	114	INR > Sum_Type.Inr
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	115	OUTL > HOLLightCompat.OUTL
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	116	OUTR > HOLLightCompat.OUTR
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	117	NONE > Datatype.None
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	118	SOME > Datatype.Some
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	119	EVEN > Parity.even_odd_class.even :: "nat \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	120	ODD > HOLLightCompat.ODD
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	121	FACT > Fact.fact_class.fact :: "nat \<Rightarrow> nat"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	122	WF > Wellfounded.wfP
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	123	NIL > List.list.Nil
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	124	CONS > List.list.Cons
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	125	APPEND > List.append
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	126	REVERSE > List.rev
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	127	LENGTH > List.length
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	128	MAP > List.map
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	129	LAST > List.last
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	130	BUTLAST > List.butlast
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	131	REPLICATE > List.replicate
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	132	ITLIST > List.foldr
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	133	list_ALL > List.list_all
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	134	ALL2 > List.list_all2
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	135	list_EX > List.list_ex
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	136	FILTER > List.filter
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	137	NULL > List.null
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	138	HD > List.hd
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	139	TL > List.tl
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	140	EL > HOLLightList.list_el
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	141	ZIP > List.zip
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	142	MAP2 > HOLLightList.map2
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	143	ITLIST2 > HOLLightList.fold2
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	144	MEM > HOLLightList.list_mem
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	145	set_of_list > List.set
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	146	IN > Set.member
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	147	INSERT > Set.insert
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	148	EMPTY > Orderings.bot_class.bot :: "'a \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	149	GABS > Hilbert_Choice.Eps
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	150	GEQ > HOL.eq
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	151	GSPEC > Set.Collect
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	152	SETSPEC > HOLLightCompat.SETSPEC
44845 5e51075cbd97 added syntactic classes for "inf" and "sup" krauss parents: 44064 diff changeset	153	UNION > Lattices.sup_class.sup :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
44860 56101fa00193 renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc. haftmann parents: 44845 diff changeset	154	UNIONS > Complete_Lattices.Sup_class.Sup :: "(('a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
44845 5e51075cbd97 added syntactic classes for "inf" and "sup" krauss parents: 44064 diff changeset	155	INTER > Lattices.inf_class.inf :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
44860 56101fa00193 renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc. haftmann parents: 44845 diff changeset	156	INTERS > Complete_Lattices.Inf_class.Inf :: "(('a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	157	DIFF > Groups.minus_class.minus :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	158	SUBSET > Orderings.ord_class.less_eq :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	159	PSUBSET > Orderings.ord_class.less :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	160	DELETE > HOLLightCompat.DELETE
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	161	DISJOINT > HOLLightCompat.DISJOINT
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	162	IMAGE > Set.image
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	163	FINITE > Finite_Set.finite
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	164	INFINITE > HOLLightCompat.INFINITE
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	165	".." > HOLLightCompat.dotdot
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	166	UNIV > Orderings.top_class.top :: "'a \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	167	MEASURE > HOLLightCompat.MEASURE
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	168	(*real_of_num > RealDef.real :: "nat => real"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	169	real_neg > Groups.uminus_class.uminus :: "real => real"
44064 5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy huffman parents: 43843 diff changeset	170	real_inv > Fields.inverse_class.inverse :: "real => real"
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	171	real_add > Groups.plus_class.plus :: "real => real => real"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	172	real_sub > Groups.minus_class.minus :: "real => real => real"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	173	real_mul > Groups.times_class.times :: "real => real => real"
44064 5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy huffman parents: 43843 diff changeset	174	real_div > Fields.inverse_class.divide :: "real => real => real"
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	175	real_lt > Orderings.ord_class.less :: "real \<Rightarrow> real \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	176	real_le > Orderings.ord_class.less_eq :: "real \<Rightarrow> real \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	177	real_gt > Orderings.ord_class.greater :: "real \<Rightarrow> real \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	178	real_ge > Orderings.ord_class.greater_eq :: "real \<Rightarrow> real \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	179	real_pow > Power.power_class.power :: "real \<Rightarrow> nat \<Rightarrow> real"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	180	real_abs > Groups.abs_class.abs :: "real \<Rightarrow> real"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	181	real_max > Orderings.ord_class.max :: "real \<Rightarrow> real \<Rightarrow> real"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	182	real_min > Orderings.ord_class.min :: "real \<Rightarrow> real \<Rightarrow> real"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	183	real_sgn > Groups.sgn_class.sgn :: "real \<Rightarrow> real"*)
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	184	(*real_of_int > RealDef.real :: "int => real"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	185	int_of_real > Archimedean_Field.floor :: "real \<Rightarrow> int"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	186	dest_int > RealDef.real :: "int => real"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	187	mk_int > Archimedean_Field.floor :: "real \<Rightarrow> int"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	188	int_lt > Orderings.ord_class.less :: "int \<Rightarrow> int \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	189	int_le > Orderings.ord_class.less_eq :: "int \<Rightarrow> int \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	190	int_gt > Orderings.ord_class.greater :: "int \<Rightarrow> int \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	191	int_ge > Orderings.ord_class.greater_eq :: "int \<Rightarrow> int \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	192	int_of_num > Nat.semiring_1_class.of_nat :: "nat \<Rightarrow> int"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	193	int_neg > Groups.uminus_class.uminus :: "int \<Rightarrow> int"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	194	int_add > Groups.plus_class.plus :: "int => int => int"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	195	int_sub > Groups.minus_class.minus :: "int => int => int"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	196	int_mul > Groups.times_class.times :: "int => int => int"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	197	int_abs > Groups.abs_class.abs :: "int \<Rightarrow> int"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	198	int_max > Orderings.ord_class.max :: "int \<Rightarrow> int \<Rightarrow> int"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	199	int_min > Orderings.ord_class.min :: "int \<Rightarrow> int \<Rightarrow> int"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	200	int_sgn > Groups.sgn_class.sgn :: "int \<Rightarrow> int"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	201	int_pow > Power.power_class.power :: "int \<Rightarrow> nat \<Rightarrow> int"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	202	int_div > HOLLightInt.hl_div :: "int \<Rightarrow> int \<Rightarrow> int"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	203	div > HOLLightInt.hl_div :: "int \<Rightarrow> int \<Rightarrow> int"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	204	mod_int > HOLLightInt.hl_mod :: "int \<Rightarrow> int \<Rightarrow> int"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	205	rem > HOLLightInt.hl_mod :: "int \<Rightarrow> int \<Rightarrow> int"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	206	int_divides > Rings.dvd_class.dvd :: "int \<Rightarrow> int \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	207	int_mod > HOLLightInt.int_mod :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	208	int_gcd > HOLLightInt.int_gcd :: "int \<times> int \<Rightarrow> int"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	209	int_coprime > HOLLightInt.int_coprime :: "int \<times> int \<Rightarrow> bool"
2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	210	eqeq > HOLLightInt.eqeq*)
17440 df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	211
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	212	;end_import
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	213
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	214	;append_dump "end"
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	215
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	216	;flush_dump
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	217
43785 2bd54d4b5f3d HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 41589 diff changeset	218	;import_segment ""
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	219
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	220	end

author	bulwahn
	Thu, 29 Mar 2012 17:40:44 +0200
changeset 47197	ed681ca1188a
parent 46879	a8b1236e0837
permissions	-rw-r--r--