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

17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	1	(* Title: HOL/Import/Generate-HOLLight/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
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	6	theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	7
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	8	;import_segment "hollight"
19064 bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	9
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	10	;setup_dump "../HOLLight" "HOLLight";
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	11
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	12	;append_dump {theory HOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin }
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	13
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	14	;import_theory hollight
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	15
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	16	;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	17	(* 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	18	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	19	(* 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	20	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	21	(* 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	22	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	23	(* 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	24	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	25	(* 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	26	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	27	(* 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	28	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	29	DEF_ASSOC MEM_ASSOC DEF_ZIP EL_TL
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	30
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	31	(* 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	32	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	33	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	34	(* UNIV *)
43843 16f2fd9103bd HOL/Import: Fix errors with _mk_list Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 43785 diff changeset	35	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	36	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	37	(* 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	38	(* 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	39	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	40	(* 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	41	(* 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	42	(* 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	43	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	44	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	45
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	;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	47	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	48	"fun" > "fun"
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	49	N_1 > Product_Type.unit
37678 0040bafffdef "prod" and "sum" replace "" and "+" respectively haftmann* parents: 37391 diff changeset	50	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	51	ind > Nat.ind
37391 476270a6c2dc tuned quotes, antiquotations and whitespace haftmann parents: 35267 diff changeset	52	num > Nat.nat
37678 0040bafffdef "prod" and "sum" replace "" and "+" respectively haftmann* parents: 37391 diff changeset	53	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	54	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	55	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	56	(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	57	(int > Int.int )
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	58
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	;const_renames
17444 a389e5892691 1) mapped .. and == constants obua parents: 17440 diff changeset	60	"==" > "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	61	"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	62	"EX" > list_EX
17444 a389e5892691 1) mapped .. and == constants obua parents: 17440 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_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	65	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	66	F > HOL.False
38864 4abe644fcea5 formerly unnamed infix equality now named HOL.eq haftmann parents: 38795 diff changeset	67	"=" > HOL.eq
38786 e46e7a9cb622 formerly unnamed infix impliciation now named HOL.implies haftmann parents: 37678 diff changeset	68	"==>" > HOL.implies
38795 848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj haftmann parents: 38786 diff changeset	69	"/\\" > HOL.conj
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj haftmann parents: 38786 diff changeset	70	"\\/" > 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	71	"!" > 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	72	"?" > 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	73	"?!" > 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	74	"~" > 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	75	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	76	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	77	ONTO > Fun.surj
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	78	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	79	"@" > 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	80	CHOICE > Hilbert_Choice.Eps
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	81	I > Fun.id
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	82	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	83	LET > HOLLightCompat.LET
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	84	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	85	"," > 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	86	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	87	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	88	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	89	"_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	90	SUC > Nat.Suc
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	91	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	92	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	93	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	94	"+" > 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	95	"*" > 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	96	"-" > 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	97	"<" > 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	98	"<=" > 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	99	">" > 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	100	">=" > 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	101	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	102	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	103	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	104	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	105	MOD > Divides.div_class.mod :: "nat \<Rightarrow> nat \<Rightarrow> nat"
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	106	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	107	BIT1 > HOLLightCompat.NUMERAL_BIT1
19064 bf19cc5a7899 fixed bugs, added caching obua parents: 17644 diff changeset	108	INL > Sum_Type.Inl
20326 cbf31171c147 fixed generator obua parents: 20275 diff changeset	109	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	110	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	111	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	112	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	113	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	114	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	115	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	116	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	117	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	118	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	119	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	120	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	121	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	122	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	123	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	124	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	125	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	126	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	127	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	128	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	129	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	130	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	131	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	132	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	133	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	134	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	135	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	136	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	137	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	138	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	139	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	140	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	141	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	142	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	143	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	144	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	145	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	146	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	147	SETSPEC > HOLLightCompat.SETSPEC
44845 5e51075cbd97 added syntactic classes for "inf" and "sup" krauss parents: 44064 diff changeset	148	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	149	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	150	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	151	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	152	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	153	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	154	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	155	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	156	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	157	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	158	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	159	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	160	".." > 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	161	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	162	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	163	(*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	164	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	165	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	166	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	167	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	168	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	169	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	170	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	171	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	172	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	173	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	174	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	175	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	176	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	177	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	178	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	179	(*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	180	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	181	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	182	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	183	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	184	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	185	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	186	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	187	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	188	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	189	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	190	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	191	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	192	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	193	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	194	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	195	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	196	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	197	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	198	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	199	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	200	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	201	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	202	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	203	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	204	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	205	eqeq > HOLLightInt.eqeq*)
17440 df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions obua parents: 17322 diff changeset	206
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	207	;end_import
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	208
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	209	;append_dump "end"
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	210
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	211	;flush_dump
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	212
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	213	;import_segment ""
17322 781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	214
781abf7011e6 Added HOLLight support to importer. obua parents: diff changeset	215	end

author	bulwahn
	Fri, 27 Jan 2012 10:31:30 +0100
changeset 46343	6d9535e52915
parent 44860	56101fa00193
child 46780	ab4f3f765f91
permissions	-rw-r--r--