nominal2: Nominal-General/nominal_library.ML@3b83960f9544 (annotated)

1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	(* Title: nominal_library.ML
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	Author: Christian Urban
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	3
1979 760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	4	Basic functions for nominal.
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	*)
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	signature NOMINAL_LIBRARY =
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	sig
2288 3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	9	val dest_listT: typ -> typ
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	10
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	val mk_minus: term -> term
1896 996d4411e95e tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability) Christian Urban <urbanc@in.tum.de> parents: 1871 diff changeset	12	val mk_plus: term -> term -> term
996d4411e95e tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability) Christian Urban <urbanc@in.tum.de> parents: 1871 diff changeset	13
1899 8e0bfb14f6bf optimised the code of define_raw_perm Christian Urban <urbanc@in.tum.de> parents: 1896 diff changeset	14	val perm_ty: typ -> typ
1871 c704d129862b moved some general function into nominal_library.ML Christian Urban <urbanc@in.tum.de> parents: 1834 diff changeset	15	val mk_perm_ty: typ -> term -> term -> term
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	val mk_perm: term -> term -> term
1834 9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	17	val dest_perm: term -> term * term
9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	18
1962 84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	19	val mk_sort_of: term -> term
1979 760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	20	val atom_ty: typ -> typ
1962 84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	21	val mk_atom_ty: typ -> term -> term
84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	22	val mk_atom: term -> term
84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	23
1979 760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	24	val supp_ty: typ -> typ
760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	25	val mk_supp_ty: typ -> term -> term
760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	26	val mk_supp: term -> term
760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	27
1834 9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	28	val mk_equiv: thm -> thm
9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	29	val safe_mk_equiv: thm -> thm
2288 3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	30
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	31	(* datatype operations *)
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	32	val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	33	val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list ->
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	34	(term * typ * typ list) list list
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	35	val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int ->
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	36	(term * typ * typ list) list
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	37	val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	38
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	39	end
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	40
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	41
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	42	structure Nominal_Library: NOMINAL_LIBRARY =
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	43	struct
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	44
2288 3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	45	(* this function should be in hologic.ML *)
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	46	fun dest_listT (Type (@{type_name list}, [T])) = T
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	47	\| dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	48
1979 760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	49	fun mk_minus p = @{term "uminus::perm => perm"} $ p;
760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	50
760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	51	fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q;
1896 996d4411e95e tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability) Christian Urban <urbanc@in.tum.de> parents: 1871 diff changeset	52
1979 760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	53	fun perm_ty ty = @{typ "perm"} --> ty --> ty;
760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	54	fun mk_perm_ty ty p trm = Const (@{const_name "permute"}, perm_ty ty) $ p $ trm;
760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	55	fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm;
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	56
1834 9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	57	fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
1979 760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	58	\| dest_perm t = raise TERM ("dest_perm", [t]);
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	59
1962 84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	60
84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	61	fun mk_sort_of t = @{term "sort_of"} $ t;
84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	62
1979 760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	63	fun atom_ty ty = ty --> @{typ "atom"};
1963 0c9ef14e9ba4 some tuning Christian Urban <urbanc@in.tum.de> parents: 1962 diff changeset	64	fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t;
1962 84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	65	fun mk_atom t = mk_atom_ty (fastype_of t) t;
84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	66
1979 760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	67
760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	68	fun supp_ty ty = ty --> @{typ "atom set"};
760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	69	fun mk_supp_ty ty t = Const (@{const_name "supp"}, supp_ty ty) $ t;
760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	70	fun mk_supp t = mk_supp_ty (fastype_of t) t;
760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	71
760257a66604 added basic functions for constructing supp-terms Christian Urban <urbanc@in.tum.de> parents: 1963 diff changeset	72
1834 9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	73	fun mk_equiv r = r RS @{thm eq_reflection};
9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	74	fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	75
1962 84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	76
2288 3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	77	( datatypes )
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	78
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	79
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	80	(* returns the type of the nth datatype *)
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	81	fun nth_dtyp descr sorts n =
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	82	Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n);
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	83
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	84	(* returns info about constructors in a datatype *)
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	85	fun all_dtyp_constrs_info descr =
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	86	map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	87
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	88	(* returns the constants of the constructors plus the
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	89	corresponding type and types of arguments *)
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	90	fun all_dtyp_constrs_types descr sorts =
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	91	let
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	92	fun aux ((ty_name, vs), (cname, args)) =
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	93	let
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	94	val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	95	val ty = Type (ty_name, vs_tys)
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	96	val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	97	in
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	98	(Const (cname, arg_tys ---> ty), ty, arg_tys)
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	99	end
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	100	in
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	101	map (map aux) (all_dtyp_constrs_info descr)
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	102	end
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	103
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	104	fun nth_dtyp_constrs_types descr sorts n =
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	105	nth (all_dtyp_constrs_types descr sorts) n
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	106
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	107
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	108	(* generates for every datatype a name str ^ dt_name
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	109	plus and index for multiple occurences of a string *)
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	110	fun prefix_dt_names descr sorts str =
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	111	let
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	112	fun get_nth_name (i, _) =
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	113	Datatype_Aux.name_of_typ (nth_dtyp descr sorts i)
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	114	in
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	115	Datatype_Prop.indexify_names
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	116	(map (prefix str o get_nth_name) descr)
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	117	end
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	118
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 1979 diff changeset	119
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	120	end (* structure *)
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	121
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	122	open Nominal_Library;

author	Christian Urban <urbanc@in.tum.de>
	Thu, 20 May 2010 21:23:53 +0100
changeset 2288	3b83960f9544
parent 1979	760257a66604
child 2289	bf748be70109
permissions	-rw-r--r--