isabelle: src/Tools/Metis/src/PortableIsabelle.sml@9625e5bfa456 (annotated)

23442 028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	1	(* ========================================================================= *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	2	(* Isabelle ML SPECIFIC FUNCTIONS *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	3	(* ========================================================================= *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	4
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	5	structure Portable :> Portable =
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	6	struct
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	7
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	8	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	9	(* The ML implementation. *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	10	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	11
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	12	val ml = ml_system;
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	13
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	14	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	15	(* Pointer equality using the run-time system. *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	16	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	17
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	18	val pointerEqual = pointer_eq;
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	19
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	20	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	21	(* Timing function applications a la Mosml.time. *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	22	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	23
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	24	val time = timeap;
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	25
24316 3880d21d6013 added CRITICAL section markup; wenzelm parents: 23442 diff changeset	26	(* ------------------------------------------------------------------------- *)
3880d21d6013 added CRITICAL section markup; wenzelm parents: 23442 diff changeset	27	(* Critical section markup (multiprocessing) *)
3880d21d6013 added CRITICAL section markup; wenzelm parents: 23442 diff changeset	28	(* ------------------------------------------------------------------------- *)
3880d21d6013 added CRITICAL section markup; wenzelm parents: 23442 diff changeset	29
24324 9625e5bfa456 NAMED_CRITICAL; wenzelm parents: 24316 diff changeset	30	fun CRITICAL e = NAMED_CRITICAL "metis" e;
24316 3880d21d6013 added CRITICAL section markup; wenzelm parents: 23442 diff changeset	31
23442 028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	32	end
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	33
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	34	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	35	(* Quotations a la Moscow ML. *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	36	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	37
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	38	datatype 'a frag = QUOTE of string \| ANTIQUOTE of 'a;

author	wenzelm
	Sat, 18 Aug 2007 13:32:26 +0200
changeset 24324	9625e5bfa456
parent 24316	3880d21d6013
child 25430	372d6749f00e
permissions	-rw-r--r--