Lines Matching refs:context
46 type context
48 val empty : context
50 val add_rewrite : Thm.thm -> context -> context
52 val add_conversion : named_conv -> context -> context
54 val add_reduction : Thm.thm -> context -> context
56 val add_judgement : Thm.thm -> context -> context
58 val simpset_frag : context -> simpLib.ssfrag
60 val simpset : context -> simpLib.simpset
62 val to_string : context -> string
64 val pp : ppstream -> context -> unit
67 (* Subtype context pairs: one for simplification, the other for *)
71 (* simplify context, and add_X2'' adds to just the normalize context. *)
76 val dest2 : context2 -> {simplify : context, normalize : context}