Lines Matching refs:fn
81 fun (f >>> g) = (f >> (fn (v,v1) => (v,g v1)))
141 List.foldl (fn (p,s') => case s' of
167 (fn (x,(l1,l2)) => if (p x) then ([],(x::l1)::l2)
182 assumes = List.map (fn (n,t) => {name=n,term=t}) a,
183 fixes = List.map (fn (ns,t) => {names=ns,tp=t}) f };
293 |> space_implode " " |> (fn v =>
306 let val assumes = fn k => e k #>
317 >> (fn (((v,a),f),a1) =>
322 val parse_mixfix = fn p_ =>
324 val prio = fn s2i => p str_ >>> s2i
328 (fn (t,(ps,p)) => Template
338 (fn (t,(ps,p)) => Binder
365 >> (fn (((v,n),ps),l) =>
374 >> (fn (((v,n),ps),l) =>
378 #> oneOf [p type_ident >>> (fn v => [v]),
389 >> (fn (((v,n),t),def) =>
398 >> (fn ((v,ns),def) =>
416 (fn (t,(a,(n,e))) => Definition {
426 #> pack #> pack >>> (fn (n,(m,ns)) =>
464 fun proof p_ = succeedP p_ #> p (proof_prefix []) #> p (fn cmd =>
476 >>> (fn (cmds,cmds1) => cmds@cmds1 |>
481 >>> (fn v1 => case v1 of
485 val parse_arity = fn _ => optional (e (keyword "(") #>
493 (fn ((t,(n,(a,(l,stmt)))),prf) =>
503 (fn ((t,(n,(a,(l,stmt)))),prf) =>
521 (fn (n,(r,p)) => InstanceR {
532 >>> (fn ((n,(q,e)),prf) =>
542 >>> (List.map (fn (ns,(t,m)) =>
545 ((p (fn t => if String.isPrefix "hide_"
555 >>> (fn (s,(opt,ns)) =>
565 (fn v => MiscCmd ("text",v)),
567 (fn v => MiscCmd ("section",v)),
569 (fn v => MiscCmd ("subsection",v)),
571 (fn v => MiscCmd ("value",v)),
573 (fn v => MiscCmd ("unused_thms",v)),
575 (fn v => MiscCmd ("ML_file",v)),
577 (fn v => MiscCmd ("setup",v)),
590 #> pack #> pack >>> (fn (ns,(a,b)) =>
597 #> expect_end >> (fn ((((_,h),n),(i,k)),b) =>
603 #> (fn v => (v >>= I,getError v));
698 fun lift f sel = fn (t1,t2) => f (sel t1,sel t2)
740 (fn T' => if is_non_image_theory T'
747 val vars = List.map (fn (s,tp) => Var ((s,0),tp))
755 fun thms_of T = List.map (fn (s,d) => (s,prop_of d))
764 let val get_consts = fn T => List.map (fn (n,(t,_)) => (n,t))
772 val is_mutually_rec_type = fn (_,i) => length (#descr i) >1
773 val check_rec = fn (n,v) => if is_mutually_rec_type (n,v)
775 val rec dtyp2typ = fn (descs,t) => case t of
784 val dt_desc = fn info => List.map (fn (_,(s,vs,eqs)) =>
786 val eqs' = List.map (fn (s,ts) =>
789 in List.foldl (fn (n,l) => case Datatype.get_info T n of
801 let val get_funs = fn T =>
804 val fun_def = (fn (pats,def) => (#2 (strip_comb pats),def))
807 in List.map (fn (c,i) => case dest_Const c of
814 val cls_names = List.map (fn n => String.substring (n,0,String.size n-
817 in List.map (fn name =>
820 (fn tm => Term.add_const_names tm [])
823 val parents = List.map (fn n => String.substring
825 (List.filter (fn n => (String.isSuffix "_class" n) andalso
827 val axioms' = List.map (fn (n,t) => (n,(HOLogic.dest_Trueprop o #2
832 val all_params = List.map (fn (s,t) => (Long_Name.base_name s,t))
834 val sub_vars = List.map (fn (s,t) => ((s,0),Free (s,t))) all_params
835 val axioms = List.map (fn (s,t) => (s,Term.subst_Vars sub_vars t))
840 let val all_locales = fn T => List.map (fn l => (#name l, #parents l))
843 (fn (c,l) => fast_string_ord (#1 c,#1 l))
849 in List.map (fn (name,ps) =>
852 (List.filter (fn (s,_) => List.exists (curry op= s) ps) locales)))
853 val params = Ord_List.subtract (fn (s,((s1,_),_)) =>
862 (fn t => (not (List.exists
863 (fn s => String.isPrefix (name ^ s) (#1 t))
865 val axioms = List.map (fn (s,t) => (s,(HOLogic.dest_Trueprop o #2
868 val fix_consts = List.map (fn (s,t) => (s, Term.subst_Vars
869 (List.map (fn ((s,tp),_) =>
871 val parse_axioms = fn v => List.map hol_forall_elim
880 val in_loc = List.filter (fn (_,t) =>
881 List.exists (fn t' => t = t') in_locale_axioms) axioms
882 val ex_loc = List.filter (fn (_,t) =>
883 not (List.exists (fn t' => t = t') in_locale_axioms)) axioms
905 val body = List.map (fn (pats,tm) => Pretty.quote (Pretty.block
907 @(List.map (fn p => Pretty.enclose "(" ")" [repr_term T p])
917 val fixes' = List.map (fn (s,tp) => Pretty.block (Pretty.breaks
920 val assumes' = List.map (fn (s,tm) => Pretty.block (Pretty.breaks
936 val fixes' = List.map (fn ((s,tp),_) => Pretty.block (Pretty.breaks
939 val assumes' = List.map (fn (s,tm) => Pretty.block (Pretty.breaks
951 let val dts = List.map (fn (s,vs,eqs) =>
955 (fn (s,vs) => Pretty.block (Pretty.breaks
967 (List.map (fn l => ((#1 l,l),#2 l)) (classes_of T))
974 (List.map (fn l => ((#1 l,l),#5 l)) (locales_of T))
988 val cmp = (fn (s,(s1,_)) =>
1003 in List.map (fn T =>
1019 List.map (fn (n,s) =>
1049 (fn (name,type_params,constructors) =>
1052 @(List.map (fn (s,tps) => XML.Elem
1060 ::(List.map(fn (pats,tm) =>
1066 (List.map (fn p =>
1068 @(List.map (fn (s,t) =>
1071 @(List.map (fn (s,t) =>
1077 (List.map (fn ((s,t),m) =>
1081 @(List.map (fn (s,t) =>
1084 @(List.map (fn (s,t) =>
1087 @(List.map (fn p =>
1093 (fn T => XML.Elem (("Import",[("name",name_of_theory T)]),[]))
1095 val axioms = List.map (fn (n,t) => XML.Elem
1098 val theorems = List.map (fn (n,t) => XML.Elem
1101 val consts = List.map (fn (n,tp) => XML.Elem