nominal2: Nominal/nominal_dt_rawperm.ML@1e6160690546 (annotated)

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: diff changeset	1	(* Title: nominal_dt_rawperm.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: diff changeset	2	Author: Cezary Kaliszyk
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: diff changeset	3	Author: Christian Urban
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: diff changeset	4
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: diff changeset	5	Definitions of the raw permutations and
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: diff changeset	6	proof that the raw datatypes are in 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: diff changeset	7	pt-class.
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: diff changeset	8	*)
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: diff changeset	9
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: diff changeset	10	signature NOMINAL_DT_RAWPERM =
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: diff changeset	11	sig
2398 1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	12	val define_raw_perms: string list -> typ list -> term list -> thm -> theory ->
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: diff changeset	13	(term list * thm list * thm list) * theory
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: diff changeset	14	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: diff changeset	15
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: diff changeset	16
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: diff changeset	17	structure Nominal_Dt_RawPerm: NOMINAL_DT_RAWPERM =
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: diff changeset	18	struct
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: diff changeset	19
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: diff changeset	20
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: diff changeset	21	( proves the two pt-type class properties )
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: diff changeset	22
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: diff changeset	23	fun prove_permute_zero lthy induct perm_defs perm_fns =
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: diff changeset	24	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: diff changeset	25	val perm_types = map (body_type o fastype_of) perm_fns
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: diff changeset	26	val perm_indnames = Datatype_Prop.make_tnames perm_types
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: diff changeset	27
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: diff changeset	28	fun single_goal ((perm_fn, T), x) =
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: diff changeset	29	HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, 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: 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: diff changeset	31	val goals =
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: diff changeset	32	HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
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: diff changeset	33	(map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
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: diff changeset	34
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: diff changeset	35	val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs)
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: diff changeset	36
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: diff changeset	37	val tac = (Datatype_Aux.indtac induct perm_indnames
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: diff changeset	38	THEN_ALL_NEW asm_simp_tac simps) 1
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: diff changeset	39	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: diff changeset	40	Goal.prove lthy perm_indnames [] goals (K tac)
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: diff changeset	41	\|> Datatype_Aux.split_conj_thm
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: diff changeset	42	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: diff changeset	43
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: diff changeset	44
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: diff changeset	45	fun prove_permute_plus lthy induct perm_defs perm_fns =
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: diff changeset	46	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: diff changeset	47	val p = Free ("p", @{typ perm})
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: diff changeset	48	val q = Free ("q", @{typ perm})
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: diff changeset	49	val perm_types = map (body_type o fastype_of) perm_fns
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: diff changeset	50	val perm_indnames = Datatype_Prop.make_tnames perm_types
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: diff changeset	51
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: diff changeset	52	fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq
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: diff changeset	53	(perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, 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: diff changeset	54
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: diff changeset	55	val goals =
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: diff changeset	56	HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
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: diff changeset	57	(map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
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: diff changeset	58
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: diff changeset	59	val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs)
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: diff changeset	60
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: diff changeset	61	val tac = (Datatype_Aux.indtac induct perm_indnames
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: diff changeset	62	THEN_ALL_NEW asm_simp_tac simps) 1
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: diff changeset	63	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: diff changeset	64	Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac)
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: diff changeset	65	\|> Datatype_Aux.split_conj_thm
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: diff changeset	66	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: diff changeset	67
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: diff changeset	68
2398 1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	69	fun mk_perm_eq ty_perm_assoc cnstr =
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: diff changeset	70	let
2398 1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	71	fun lookup_perm p (ty, arg) =
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	72	case (AList.lookup (op=) ty_perm_assoc ty) of
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	73	SOME perm => perm $ p $ arg
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	74	\| NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	75
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	76	val p = Free ("p", @{typ perm})
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	77	val (arg_tys, ty) =
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	78	fastype_of cnstr
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	79	\|> strip_type
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	80
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	81	val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	82	val args = map Free (arg_names ~~ arg_tys)
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: diff changeset	83
2398 1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	84	val lhs = lookup_perm p (ty, list_comb (cnstr, args))
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	85	val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args))
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	86
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	87	val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	88	in
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	89	(Attrib.empty_binding, eq)
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	90	end
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	91
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: diff changeset	92
2398 1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	93	fun define_raw_perms full_ty_names tys constrs induct_thm thy =
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	94	let
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	95	val perm_fn_names = full_ty_names
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	96	\|> map Long_Name.base_name
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	97	\|> map (prefix "permute_")
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: diff changeset	98
2398 1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	99	val perm_fn_types = map perm_ty tys
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	100	val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types)
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	101	val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	102
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	103	val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs
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: diff changeset	104
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: diff changeset	105	val lthy =
2398 1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	106	Class.instantiation (full_ty_names, [], @{sort pt}) thy
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: 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: diff changeset	108	val ((perm_funs, perm_eq_thms), lthy') =
2398 1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	109	Primrec.add_primrec perm_fn_binds perm_eqs lthy;
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: diff changeset	110
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: diff changeset	111	val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs
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: diff changeset	112	val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs
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: diff changeset	113
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: diff changeset	114	fun tac _ (_, _, simps) =
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: diff changeset	115	Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
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: diff changeset	116
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: diff changeset	117	fun morphism phi (fvs, dfs, simps) =
2398 1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	118	(map (Morphism.term phi) fvs,
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	119	map (Morphism.thm phi) dfs,
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	120	map (Morphism.thm phi) simps);
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: diff changeset	121	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: diff changeset	122	lthy'
2396 f2f611daf480 updated to Isabelle 12th Aug Christian Urban <urbanc@in.tum.de> parents: 2295 diff changeset	123	\|> Class.prove_instantiation_exit_result morphism tac
2398 1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	124	(perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms)
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: diff changeset	125	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: diff changeset	126
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: diff changeset	127
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: diff changeset	128	end (* structure *)
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: diff changeset	129

author	Christian Urban <urbanc@in.tum.de>
	Sat, 14 Aug 2010 23:33:23 +0800
changeset 2398	1e6160690546
parent 2396	f2f611daf480
child 2401	7645e18e8b19
permissions	-rw-r--r--