1.1 --- a/src/HOL/Library/Fset.thy Fri Jun 18 22:41:16 2010 +0200
1.2 +++ b/src/HOL/Library/Fset.thy Sun Jun 20 22:01:22 2010 +0200
1.3 @@ -7,22 +7,26 @@
1.4 imports More_Set More_List
1.5 begin
1.6
1.7 -declare mem_def [simp]
1.8 -
1.9 subsection {* Lifting *}
1.10
1.11 -datatype 'a fset = Fset "'a set"
1.12 +typedef (open) 'a fset = "UNIV :: 'a set set"
1.13 + morphisms member Fset by rule+
1.14
1.15 -primrec member :: "'a fset \<Rightarrow> 'a set" where
1.16 +lemma member_Fset [simp]:
1.17 "member (Fset A) = A"
1.18 -
1.19 -lemma member_inject [simp]:
1.20 - "member A = member B \<Longrightarrow> A = B"
1.21 - by (cases A, cases B) simp
1.22 + by (rule Fset_inverse) rule
1.23
1.24 lemma Fset_member [simp]:
1.25 "Fset (member A) = A"
1.26 - by (cases A) simp
1.27 + by (rule member_inverse)
1.28 +
1.29 +declare member_inject [simp]
1.30 +
1.31 +lemma Fset_inject [simp]:
1.32 + "Fset A = Fset B \<longleftrightarrow> A = B"
1.33 + by (simp add: Fset_inject)
1.34 +
1.35 +declare mem_def [simp]
1.36
1.37 definition Set :: "'a list \<Rightarrow> 'a fset" where
1.38 "Set xs = Fset (set xs)"
1.39 @@ -56,6 +60,27 @@
1.40 then show ?thesis by (simp add: image_def)
1.41 qed
1.42
1.43 +definition (in term_syntax)
1.44 + setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
1.45 + \<Rightarrow> 'a fset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
1.46 + [code_unfold]: "setify xs = Code_Evaluation.valtermify Set {\<cdot>} xs"
1.47 +
1.48 +notation fcomp (infixl "o>" 60)
1.49 +notation scomp (infixl "o\<rightarrow>" 60)
1.50 +
1.51 +instantiation fset :: (random) random
1.52 +begin
1.53 +
1.54 +definition
1.55 + "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>xs. Pair (setify xs))"
1.56 +
1.57 +instance ..
1.58 +
1.59 +end
1.60 +
1.61 +no_notation fcomp (infixl "o>" 60)
1.62 +no_notation scomp (infixl "o\<rightarrow>" 60)
1.63 +
1.64
1.65 subsection {* Lattice instantiation *}
1.66
1.67 @@ -117,11 +142,11 @@
1.68
1.69 lemma empty_Set [code]:
1.70 "bot = Set []"
1.71 - by simp
1.72 + by (simp add: Set_def)
1.73
1.74 lemma UNIV_Set [code]:
1.75 "top = Coset []"
1.76 - by simp
1.77 + by (simp add: Coset_def)
1.78
1.79 definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
1.80 [simp]: "insert x A = Fset (Set.insert x (member A))"
1.81 @@ -198,9 +223,16 @@
1.82 "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a fset)"
1.83 by (fact less_le_not_le)
1.84
1.85 -lemma eq_fset_subfset_eq [code]:
1.86 - "eq_class.eq A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
1.87 - by (cases A, cases B) (simp add: eq set_eq)
1.88 +instantiation fset :: (type) eq
1.89 +begin
1.90 +
1.91 +definition
1.92 + "eq_fset A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
1.93 +
1.94 +instance proof
1.95 +qed (simp add: eq_fset_def set_eq [symmetric])
1.96 +
1.97 +end
1.98
1.99
1.100 subsection {* Functorial operations *}
1.101 @@ -276,22 +308,6 @@
1.102 end
1.103
1.104
1.105 -subsection {* Misc operations *}
1.106 -
1.107 -lemma size_fset [code]:
1.108 - "fset_size f A = 0"
1.109 - "size A = 0"
1.110 - by (cases A, simp) (cases A, simp)
1.111 -
1.112 -lemma fset_case_code [code]:
1.113 - "fset_case f A = f (member A)"
1.114 - by (cases A) simp
1.115 -
1.116 -lemma fset_rec_code [code]:
1.117 - "fset_rec f A = f (member A)"
1.118 - by (cases A) simp
1.119 -
1.120 -
1.121 subsection {* Simplified simprules *}
1.122
1.123 lemma is_empty_simp [simp]:
1.124 @@ -312,7 +328,7 @@
1.125 declare mem_def [simp del]
1.126
1.127
1.128 -hide_const (open) is_empty insert remove map filter forall exists card
1.129 +hide_const (open) setify is_empty insert remove map filter forall exists card
1.130 Inter Union
1.131
1.132 end
2.1 --- a/src/HOL/Tools/record.ML Fri Jun 18 22:41:16 2010 +0200
2.2 +++ b/src/HOL/Tools/record.ML Sun Jun 20 22:01:22 2010 +0200
2.3 @@ -64,7 +64,7 @@
2.4
2.5 signature ISO_TUPLE_SUPPORT =
2.6 sig
2.7 - val add_iso_tuple_type: bstring * (string * sort) list ->
2.8 + val add_iso_tuple_type: binding * (string * sort) list ->
2.9 typ * typ -> theory -> (term * term) * theory
2.10 val mk_cons_tuple: term * term -> term
2.11 val dest_cons_tuple: term -> term * term
2.12 @@ -80,7 +80,7 @@
2.13 val iso_tuple_intro = @{thm isomorphic_tuple_intro};
2.14 val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
2.15
2.16 -val tuple_iso_tuple = (@{const_name tuple_iso_tuple}, @{thm tuple_iso_tuple});
2.17 +val tuple_iso_tuple = (@{const_name Record.tuple_iso_tuple}, @{thm tuple_iso_tuple});
2.18
2.19 fun named_cterm_instantiate values thm =
2.20 let
2.21 @@ -101,21 +101,21 @@
2.22 fun merge data = Symtab.merge Thm.eq_thm_prop data; (* FIXME handle Symtab.DUP ?? *)
2.23 );
2.24
2.25 -fun do_typedef name repT alphas thy =
2.26 +fun do_typedef b repT alphas thy =
2.27 let
2.28 - fun get_thms thy name =
2.29 + val (b_constr, b_proj) = (Binding.prefix_name "make_" b, Binding.prefix_name "dest_" b);
2.30 + fun get_thms thy tyco =
2.31 let
2.32 - val [({Abs_name, abs_type = absT, ...}, {Rep_inject, Abs_inverse, ...})] =
2.33 - Typedef.get_info_global thy name;
2.34 - val rewrite_rule =
2.35 - MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}];
2.36 + val SOME { vs, constr, typ = repT, proj_inject, proj_constr, ... } =
2.37 + Typecopy.get_info thy tyco;
2.38 + val absT = Type (tyco, map TFree vs);
2.39 in
2.40 - (map rewrite_rule [Rep_inject, Abs_inverse], Const (Abs_name, repT --> absT), absT)
2.41 + ((proj_inject, proj_constr), Const (constr, repT --> absT), absT)
2.42 end;
2.43 in
2.44 thy
2.45 - |> Typecopy.typecopy (Binding.name name, alphas) repT NONE
2.46 - |-> (fn (name, _) => `(fn thy => get_thms thy name))
2.47 + |> Typecopy.typecopy (b, alphas) repT b_constr b_proj
2.48 + |-> (fn (tyco, _) => `(fn thy => get_thms thy tyco))
2.49 end;
2.50
2.51 fun mk_cons_tuple (left, right) =
2.52 @@ -124,21 +124,21 @@
2.53 val prodT = HOLogic.mk_prodT (leftT, rightT);
2.54 val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]);
2.55 in
2.56 - Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $
2.57 + Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $
2.58 Const (fst tuple_iso_tuple, isomT) $ left $ right
2.59 end;
2.60
2.61 -fun dest_cons_tuple (Const (@{const_name iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
2.62 +fun dest_cons_tuple (Const (@{const_name Record.iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
2.63 | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
2.64
2.65 -fun add_iso_tuple_type (name, alphas) (leftT, rightT) thy =
2.66 +fun add_iso_tuple_type (b, alphas) (leftT, rightT) thy =
2.67 let
2.68 val repT = HOLogic.mk_prodT (leftT, rightT);
2.69
2.70 - val (([rep_inject, abs_inverse], absC, absT), typ_thy) =
2.71 + val (((rep_inject, abs_inverse), absC, absT), typ_thy) =
2.72 thy
2.73 - |> do_typedef name repT alphas
2.74 - ||> Sign.add_path name;
2.75 + |> do_typedef b repT alphas
2.76 + ||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*)
2.77
2.78 (*construct a type and body for the isomorphism constant by
2.79 instantiating the theorem to which the definition will be applied*)
2.80 @@ -146,7 +146,7 @@
2.81 rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro;
2.82 val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
2.83 val isomT = fastype_of body;
2.84 - val isom_binding = Binding.name (name ^ isoN);
2.85 + val isom_binding = Binding.suffix_name isoN b;
2.86 val isom_name = Sign.full_name typ_thy isom_binding;
2.87 val isom = Const (isom_name, isomT);
2.88
2.89 @@ -157,7 +157,7 @@
2.90 [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
2.91
2.92 val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
2.93 - val cons = Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
2.94 + val cons = Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
2.95
2.96 val thm_thy =
2.97 cdef_thy
2.98 @@ -1654,7 +1654,7 @@
2.99 val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
2.100 val ((_, cons), thy') = thy
2.101 |> Iso_Tuple_Support.add_iso_tuple_type
2.102 - (suffix suff base_name, alphas_zeta) (fastype_of left, fastype_of right);
2.103 + (Binding.suffix_name suff (Binding.name base_name), alphas_zeta) (fastype_of left, fastype_of right);
2.104 in
2.105 (cons $ left $ right, (thy', i + 1))
2.106 end;
2.107 @@ -1846,8 +1846,9 @@
2.108
2.109 fun record_definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
2.110 let
2.111 + val prefix = Binding.name_of binding;
2.112 val name = Sign.full_name thy binding;
2.113 - val full = Sign.full_name_path thy (Binding.name_of binding); (* FIXME Binding.qualified (!?) *)
2.114 + val full = Sign.full_name_path thy prefix;
2.115
2.116 val bfields = map (fn (x, T, _) => (x, T)) raw_fields;
2.117 val field_syntax = map #3 raw_fields;
2.118 @@ -1859,7 +1860,7 @@
2.119 val parent_fields_len = length parent_fields;
2.120 val parent_variants =
2.121 Name.variant_list [moreN, rN, rN ^ "'", wN] (map Long_Name.base_name parent_names);
2.122 - val parent_vars = ListPair.map Free (parent_variants, parent_types);
2.123 + val parent_vars = map2 (curry Free) parent_variants parent_types;
2.124 val parent_len = length parents;
2.125
2.126 val fields = map (apfst full) bfields;
2.127 @@ -1871,7 +1872,7 @@
2.128 val variants =
2.129 Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
2.130 (map (Binding.name_of o fst) bfields);
2.131 - val vars = ListPair.map Free (variants, types);
2.132 + val vars = map2 (curry Free) variants types;
2.133 val named_vars = names ~~ vars;
2.134 val idxms = 0 upto len;
2.135
2.136 @@ -2090,13 +2091,13 @@
2.137 map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
2.138
2.139 (*updates*)
2.140 - fun mk_upd_prop (i, (c, T)) =
2.141 + fun mk_upd_prop i (c, T) =
2.142 let
2.143 val x' = Free (Name.variant all_variants (Long_Name.base_name c ^ "'"), T --> T);
2.144 val n = parent_fields_len + i;
2.145 val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
2.146 in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
2.147 - val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
2.148 + val upd_conv_props = map2 mk_upd_prop idxms fields_more;
2.149
2.150 (*induct*)
2.151 val induct_scheme_prop =
3.1 --- a/src/HOL/Tools/typecopy.ML Fri Jun 18 22:41:16 2010 +0200
3.2 +++ b/src/HOL/Tools/typecopy.ML Sun Jun 20 22:01:22 2010 +0200
3.3 @@ -6,9 +6,9 @@
3.4
3.5 signature TYPECOPY =
3.6 sig
3.7 - type info = { vs: (string * sort) list, constr: string, typ: typ,
3.8 - inject: thm, proj: string * typ, proj_def: thm }
3.9 - val typecopy: binding * (string * sort) list -> typ -> (binding * binding) option
3.10 + type info = { vs: (string * sort) list, typ: typ, constr: string, proj: string,
3.11 + constr_inject: thm, proj_inject: thm, constr_proj: thm, proj_constr: thm }
3.12 + val typecopy: binding * (string * sort) list -> typ -> binding -> binding
3.13 -> theory -> (string * info) * theory
3.14 val get_info: theory -> string -> info option
3.15 val interpretation: (string -> theory -> theory) -> theory -> theory
3.16 @@ -23,14 +23,16 @@
3.17
3.18 type info = {
3.19 vs: (string * sort) list,
3.20 + typ: typ,
3.21 constr: string,
3.22 - typ: typ,
3.23 - inject: thm,
3.24 - proj: string * typ,
3.25 - proj_def: thm
3.26 + proj: string,
3.27 + constr_inject: thm,
3.28 + proj_inject: thm,
3.29 + constr_proj: thm,
3.30 + proj_constr: thm
3.31 };
3.32
3.33 -structure TypecopyData = Theory_Data
3.34 +structure Typecopy_Data = Theory_Data
3.35 (
3.36 type T = info Symtab.table;
3.37 val empty = Symtab.empty;
3.38 @@ -38,7 +40,7 @@
3.39 fun merge data = Symtab.merge (K true) data;
3.40 );
3.41
3.42 -val get_info = Symtab.lookup o TypecopyData.get;
3.43 +val get_info = Symtab.lookup o Typecopy_Data.get;
3.44
3.45
3.46 (* interpretation of type copies *)
3.47 @@ -49,40 +51,42 @@
3.48
3.49 (* introducing typecopies *)
3.50
3.51 -fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
3.52 +fun add_info tyco vs (({ rep_type, Abs_name, Rep_name, ...},
3.53 + { Abs_inject, Rep_inject, Abs_inverse, Rep_inverse, ... }) : Typedef.info) thy =
3.54 + let
3.55 + val exists_thm =
3.56 + UNIV_I
3.57 + |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];
3.58 + val constr_inject = Abs_inject OF [exists_thm, exists_thm];
3.59 + val proj_constr = Abs_inverse OF [exists_thm];
3.60 + val info = {
3.61 + vs = vs,
3.62 + typ = rep_type,
3.63 + constr = Abs_name,
3.64 + proj = Rep_name,
3.65 + constr_inject = constr_inject,
3.66 + proj_inject = Rep_inject,
3.67 + constr_proj = Rep_inverse,
3.68 + proj_constr = proj_constr
3.69 + };
3.70 + in
3.71 + thy
3.72 + |> (Typecopy_Data.map o Symtab.update_new) (tyco, info)
3.73 + |> Typecopy_Interpretation.data tyco
3.74 + |> pair (tyco, info)
3.75 + end
3.76 +
3.77 +fun typecopy (raw_tyco, raw_vs) raw_ty constr proj thy =
3.78 let
3.79 val ty = Sign.certify_typ thy raw_ty;
3.80 val ctxt = ProofContext.init_global thy |> Variable.declare_typ ty;
3.81 val vs = map (ProofContext.check_tfree ctxt) raw_vs;
3.82 val tac = Tactic.rtac UNIV_witness 1;
3.83 - fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
3.84 - Rep_name = c_rep, ...}, { Abs_inject = inject, Abs_inverse = inverse, ... })
3.85 - : Typedef.info) thy =
3.86 - let
3.87 - val exists_thm =
3.88 - UNIV_I
3.89 - |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global ty_rep))] [];
3.90 - val inject' = inject OF [exists_thm, exists_thm];
3.91 - val proj_def = inverse OF [exists_thm];
3.92 - val info = {
3.93 - vs = vs,
3.94 - constr = c_abs,
3.95 - typ = ty_rep,
3.96 - inject = inject',
3.97 - proj = (c_rep, ty_abs --> ty_rep),
3.98 - proj_def = proj_def
3.99 - };
3.100 - in
3.101 - thy
3.102 - |> (TypecopyData.map o Symtab.update_new) (tyco, info)
3.103 - |> Typecopy_Interpretation.data tyco
3.104 - |> pair (tyco, info)
3.105 - end
3.106 in
3.107 thy
3.108 |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
3.109 - (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
3.110 - |-> (fn (tyco, info) => add_info tyco info)
3.111 + (HOLogic.mk_UNIV ty) (SOME (proj, constr)) tac
3.112 + |-> (fn (tyco, info) => add_info tyco vs info)
3.113 end;
3.114
3.115
3.116 @@ -90,10 +94,8 @@
3.117
3.118 fun add_default_code tyco thy =
3.119 let
3.120 - val SOME { constr = c, proj = (proj, _), proj_def = proj_eq, vs = vs,
3.121 - typ = ty_rep, ... } = get_info thy tyco;
3.122 - (* FIXME handle multiple typedef interpretations (!??) *)
3.123 - val [(_, { Rep_inject = proj_inject, ... })] = Typedef.get_info_global thy tyco;
3.124 + val SOME { vs, typ = ty_rep, constr = c, proj, proj_constr, proj_inject, ... } =
3.125 + get_info thy tyco;
3.126 val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c));
3.127 val ty = Type (tyco, map TFree vs);
3.128 val proj = Const (proj, ty --> ty_rep);
3.129 @@ -113,7 +115,7 @@
3.130 in
3.131 thy
3.132 |> Code.add_datatype [constr]
3.133 - |> Code.add_eqn proj_eq
3.134 + |> Code.add_eqn proj_constr
3.135 |> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq])
3.136 |> `(fn lthy => Syntax.check_term lthy eq)
3.137 |-> (fn eq => Specification.definition
4.1 --- a/src/Pure/Isar/locale.ML Fri Jun 18 22:41:16 2010 +0200
4.2 +++ b/src/Pure/Isar/locale.ML Sun Jun 20 22:01:22 2010 +0200
4.3 @@ -73,6 +73,7 @@
4.4 val add_dependency: string -> string * morphism -> morphism -> theory -> theory
4.5
4.6 (* Diagnostic *)
4.7 + val all_locales: theory -> string list
4.8 val print_locales: theory -> unit
4.9 val print_locale: theory -> bool -> xstring -> unit
4.10 val print_registrations: theory -> string -> unit
4.11 @@ -149,10 +150,6 @@
4.12 fun change_locale name =
4.13 Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
4.14
4.15 -fun print_locales thy =
4.16 - Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
4.17 - |> Pretty.writeln;
4.18 -
4.19
4.20 (*** Primitive operations ***)
4.21
4.22 @@ -343,20 +340,6 @@
4.23 activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
4.24 ([], Context.Proof (ProofContext.init_global thy)) |-> put_idents |> Context.proof_of;
4.25
4.26 -fun print_locale thy show_facts raw_name =
4.27 - let
4.28 - val name = intern thy raw_name;
4.29 - val ctxt = init name thy;
4.30 - fun cons_elem (elem as Notes _) = show_facts ? cons elem
4.31 - | cons_elem elem = cons elem;
4.32 - val elems =
4.33 - activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
4.34 - |> snd |> rev;
4.35 - in
4.36 - Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
4.37 - |> Pretty.writeln
4.38 - end;
4.39 -
4.40
4.41 (*** Registrations: interpretations in theories ***)
4.42
4.43 @@ -458,15 +441,6 @@
4.44 in roundup thy activate export dep (get_idents context, context) |-> put_idents end;
4.45
4.46
4.47 -(* Diagnostic *)
4.48 -
4.49 -fun print_registrations thy raw_name =
4.50 - (case these_registrations thy (intern thy raw_name) of
4.51 - [] => Pretty.str ("no interpretations")
4.52 - | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
4.53 - |> Pretty.writeln;
4.54 -
4.55 -
4.56 (* Add and extend registrations *)
4.57
4.58 fun amend_registration (name, morph) mixin export thy =
4.59 @@ -595,4 +569,33 @@
4.60 Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
4.61 "back-chain all introduction rules of locales"));
4.62
4.63 +
4.64 +(*** diagnostic commands and interfaces ***)
4.65 +
4.66 +fun all_locales thy = map #1 (Name_Space.extern_table (Locales.get thy));
4.67 +
4.68 +fun print_locales thy =
4.69 + Pretty.strs ("locales:" :: all_locales thy)
4.70 + |> Pretty.writeln;
4.71 +
4.72 +fun print_locale thy show_facts raw_name =
4.73 + let
4.74 + val name = intern thy raw_name;
4.75 + val ctxt = init name thy;
4.76 + fun cons_elem (elem as Notes _) = show_facts ? cons elem
4.77 + | cons_elem elem = cons elem;
4.78 + val elems =
4.79 + activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
4.80 + |> snd |> rev;
4.81 + in
4.82 + Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
4.83 + |> Pretty.writeln
4.84 + end;
4.85 +
4.86 +fun print_registrations thy raw_name =
4.87 + (case these_registrations thy (intern thy raw_name) of
4.88 + [] => Pretty.str ("no interpretations")
4.89 + | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
4.90 + |> Pretty.writeln;
4.91 +
4.92 end;