nominal2: Quot/Examples/AbsRepTest.thy@3a48ffcf0f9a (annotated)

779 3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory AbsRepTest
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
790 3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	5	ML {* open Quotient_Term *}
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	6
786 d6407afb913c used Local_Theory.declaration for storing quotdata Christian Urban <urbanc@in.tum.de> parents: 783 diff changeset	7	print_maps
d6407afb913c used Local_Theory.declaration for storing quotdata Christian Urban <urbanc@in.tum.de> parents: 783 diff changeset	8
790 3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	9
779 3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	quotient_type
787 5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	11	'a fset = "'a list" / "\<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"
5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	12	apply(rule equivpI)
5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	13	unfolding reflp_def symp_def transp_def
790 3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	14	by auto
787 5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	15
5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	16	quotient_type
5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	17	'a foo = "('a * 'a) list" / "\<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"
779 3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	apply(rule equivpI)
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	unfolding reflp_def symp_def transp_def
790 3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	20	by auto
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	21
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	22	quotient_type
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	23	'a bar = "('a * int) list" / "\<lambda>(xs::('a * int) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	24	apply(rule equivpI)
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	25	unfolding reflp_def symp_def transp_def
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	26	by auto
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	27
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	28	fun
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	29	intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	30	where
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	31	"intrel (x, y) (u, v) = (x + v = u + y)"
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	32
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	33	quotient_type int = "nat \<times> nat" / intrel
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	34	by (auto simp add: equivp_def expand_fun_eq)
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	35
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	36	print_quotients
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	37
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	38	ML {*
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	39	absrep_fun_chk absF @{context}
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	40	(@{typ "('a * 'a) list"},
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	41	@{typ "'a foo"})
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	42	\|> Syntax.string_of_term @{context}
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	43	\|> writeln
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	44	*}
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	45
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	46	(* PROBLEM
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	47	ML {*
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	48	absrep_fun_chk absF @{context}
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	49	(@{typ "(('a list) * int) list"},
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	50	@{typ "('a fset) bar"})
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	51	\|> Syntax.string_of_term @{context}
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	52	\|> writeln
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	53	})
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	54
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	55	ML {*
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	56	absrep_fun_chk absF @{context}
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	57	(@{typ "('a list) list"},
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	58	@{typ "('a fset) fset"})
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	59	\|> Syntax.string_of_term @{context}
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	60	\|> writeln
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	61	*}
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	62
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	63	ML {*
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	64	absrep_fun_chk absF @{context}
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	65	(@{typ "nat \<times> nat"},
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	66	@{typ "int"})
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	67	\|> Syntax.string_of_term @{context}
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	68	\|> writeln
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	69	*}
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	70
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	71
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	72	term abs_foo
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	73	term rep_foo
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	74	term "abs_foo o map (prod_fun id id)"
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	75	term "map (prod_fun id id) o rep_foo"
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	76
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	77	ML {*
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	78	absrep_fun_chk absF @{context}
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	79	(@{typ "('a * 'a) list"},
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	80	@{typ "'a foo"})
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	81	\|> Syntax.string_of_term @{context}
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	82	\|> writeln
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	83	*}
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	84
3a48ffcf0f9a generalised absrep function; needs consolidation Christian Urban <urbanc@in.tum.de> parents: 787 diff changeset	85	typ "('a fset) foo"
779 3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	86
783 06e17083e90b modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants Christian Urban <urbanc@in.tum.de> parents: 780 diff changeset	87	print_quotients
06e17083e90b modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants Christian Urban <urbanc@in.tum.de> parents: 780 diff changeset	88
06e17083e90b modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants Christian Urban <urbanc@in.tum.de> parents: 780 diff changeset	89	ML{*
06e17083e90b modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants Christian Urban <urbanc@in.tum.de> parents: 780 diff changeset	90	Quotient_Info.quotient_rules_get @{context}
06e17083e90b modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants Christian Urban <urbanc@in.tum.de> parents: 780 diff changeset	91	*}
06e17083e90b modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants Christian Urban <urbanc@in.tum.de> parents: 780 diff changeset	92
06e17083e90b modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants Christian Urban <urbanc@in.tum.de> parents: 780 diff changeset	93	print_quotients
06e17083e90b modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants Christian Urban <urbanc@in.tum.de> parents: 780 diff changeset	94
779 3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	95	ML {*
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	96	open Quotient_Term;
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	97	*}
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	98
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	99	ML {*
787 5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	100	absrep_fun_chk absF @{context}
5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	101	(@{typ "(('a * 'a) list) list"},
5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	102	@{typ "(('a * 'a) fset) fset"})
779 3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	103	\|> Syntax.string_of_term @{context}
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	104	\|> writeln
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	105	*}
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	106
787 5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	107	(*
5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	108	ML {*
5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	109	absrep_fun_chk absF @{context}
5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	110	(@{typ "('a * 'a) list"},
5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	111	@{typ "'a foo"})
5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	112	\|> Syntax.string_of_term @{context}
5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	113	\|> writeln
5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	114	*}
5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	115	*)
5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given Christian Urban <urbanc@in.tum.de> parents: 786 diff changeset	116
779 3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	117	term "option_map (prod_fun (abs_fset \<circ> map abs_int) id)"
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	118	term "option_map (prod_fun (map rep_int \<circ> rep_fset) id)"
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	119	term "option_map (map rep_int \<circ> rep_fset)"
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	120	term "option_map (abs_fset o (map abs_int))"
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	121	term "abs_fset"
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	122
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	123	ML {*
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	124	absrep_fun_chk absF @{context} (@{typ "(nat * nat) list"}, @{typ "int fset"})
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	125	\|> Syntax.string_of_term @{context}
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	126	\|> writeln
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	127	*}
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	128
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	129	term "map abs_int"
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	130	term "abs_fset o map abs_int"
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	131
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	132
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	133	ML {*
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	134	absrep_fun_chk absF @{context} (@{typ "('a list) list"}, @{typ "('a fset) fset"})
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	135	\|> Syntax.string_of_term @{context}
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	136	\|> writeln
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	137	*}
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	138
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	139	ML {*
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	140	absrep_fun_chk absF @{context} (@{typ "('a list) list \<Rightarrow> 'a"}, @{typ "('a fset) fset \<Rightarrow> 'a"})
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	141	\|> Syntax.string_of_term @{context}
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	142	\|> writeln
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	143	*}
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	144
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file Christian Urban <urbanc@in.tum.de> parents: diff changeset	145	end

author	Christian Urban <urbanc@in.tum.de>
	Sat, 26 Dec 2009 07:15:30 +0100 (2009-12-26)
changeset 790	3a48ffcf0f9a
parent 787	5cf83fa5b36c
child 795	a28f805df355
permissions	-rw-r--r--