/seL4-l4v-master/isabelle/src/Pure/General/ |
H A D | logger.scala | 18 def apply(msg: => String): Unit 21 Timing.timeit(message, enabled, apply(_))(e) 26 def apply(msg: => String) { } 31 def apply(msg: => String) { synchronized { File.append(path, msg + "\n") } }
|
H A D | value.scala | 14 def apply(x: scala.Boolean): java.lang.String = x.toString 38 def apply(x: scala.Int): java.lang.String = Library.signed_string_of_int(x) 48 def apply(x: scala.Long): java.lang.String = Library.signed_string_of_long(x) 58 def apply(x: scala.Double): java.lang.String = x.toString 68 def apply(t: Time): java.lang.String =
|
/seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
H A D | logger.scala | 18 def apply(msg: => String): Unit 21 Timing.timeit(message, enabled, apply(_))(e) 26 def apply(msg: => String) { } 31 def apply(msg: => String) { synchronized { File.append(path, msg + "\n") } }
|
H A D | value.scala | 14 def apply(x: scala.Boolean): java.lang.String = x.toString 38 def apply(x: scala.Int): java.lang.String = Library.signed_string_of_int(x) 48 def apply(x: scala.Long): java.lang.String = Library.signed_string_of_long(x) 58 def apply(x: scala.Double): java.lang.String = x.toString 68 def apply(t: Time): java.lang.String =
|
/seL4-l4v-master/isabelle/src/Pure/PIDE/ |
H A D | document_id.scala | 22 def apply(id: Generic): String = Value.Long.apply(id)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/PIDE/ |
H A D | document_id.scala | 22 def apply(id: Generic): String = Value.Long.apply(id)
|
/seL4-l4v-master/isabelle/src/Pure/Concurrent/ |
H A D | counter.scala | 22 def apply(): Counter.ID = synchronized {
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Concurrent/ |
H A D | counter.scala | 22 def apply(): Counter.ID = synchronized {
|
/seL4-l4v-master/isabelle/src/Tools/Graphview/ |
H A D | popups.scala | 19 def apply( 34 def apply = 40 def apply = 46 def apply = 52 def apply = 81 def apply = 100 def apply = 117 new Action("Remove all filters") { def apply = graphview.model.Mutators(Nil) }).peer) 142 def apply = graph_panel.fit_to_window() }).peer
|
H A D | metrics.scala | 30 def apply(font: Font): Metrics = new Metrics(font) 32 val default: Metrics = apply(new Font("Helvetica", Font.PLAIN, 12)) 60 def apply(s: String): Double = if (s == "\n") 1.0 else string_bounds(s).getWidth / unit
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Graphview/ |
H A D | popups.scala | 19 def apply( 34 def apply = 40 def apply = 46 def apply = 52 def apply = 81 def apply = 100 def apply = 117 new Action("Remove all filters") { def apply = graphview.model.Mutators(Nil) }).peer) 142 def apply = graph_panel.fit_to_window() }).peer
|
H A D | metrics.scala | 30 def apply(font: Font): Metrics = new Metrics(font) 32 val default: Metrics = apply(new Font("Helvetica", Font.PLAIN, 12)) 60 def apply(s: String): Double = if (s == "\n") 1.0 else string_bounds(s).getWidth / unit
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/step/ |
H A D | m0_stepLib.sig | 18 fun pev s = (print (s ^ "\n"); Count.apply ev s); 19 val _ = Count.apply (List.map ev) (list_instructions ()) 20 val _ = Count.apply (List.map (Lib.total pev)) (list_instructions ())
|
/seL4-l4v-master/isabelle/src/Pure/System/ |
H A D | getopts.scala | 12 def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts = 41 try { options(opt)._2.apply(opt_arg.mkString) } 67 def apply(args: List[String]): List[String] = getopts(args.map(_.toList)).map(_.mkString) 68 def apply(args: Array[String]): List[String] = apply(args.toList)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/System/ |
H A D | getopts.scala | 12 def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts = 41 try { options(opt)._2.apply(opt_arg.mkString) } 67 def apply(args: List[String]): List[String] = getopts(args.map(_.toList)).map(_.mkString) 68 def apply(args: Array[String]): List[String] = apply(args.toList)
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/step/ |
H A D | arm_stepLib.sig | 20 fun pev s = (print (s ^ "\n"); Count.apply ev s); 21 val _ = Count.apply (List.map ev) (list_instructions ()) 22 val _ = Count.apply (List.map (Lib.total pev)) (list_instructions ())
|
/seL4-l4v-master/HOL4/examples/miller/miller/ |
H A D | miller_rabinTools.sml | 36 Count.apply COMPOSITE_PROVER ``91 : num``; 37 Count.apply COMPOSITE_PROVER ``123 : num``; 39 Count.apply COMPOSITE_PROVER ``2 EXP (2 EXP 5) + 1``; 41 Count.apply COMPOSITE_PROVER ``2 EXP (2 EXP 6) + 1``; 43 Count.apply COMPOSITE_PROVER ``2 EXP (2 EXP 7) + 1``; 45 Count.apply COMPOSITE_PROVER ``2 EXP (2 EXP 8) + 1``;
|
/seL4-l4v-master/HOL4/src/portableML/poly/concurrent/ |
H A D | Timeout.sml | 10 val apply: Time.time -> ('a -> 'b) -> 'a -> 'b value 18 fun apply timeout f x = function
|
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | selftest.sml | 83 val tsar_anc_thm = Count.apply (TC_CONV tsarto_CONV) tsar_tc; 86 val tsar_enum_fmap = Count.apply (FMAPAL_TO_fmap_CONV tsarto_CONV) 92 (Count.apply (MAP_ELEM_CONV (RAND_CONV (ENUMERAL_TO_DISPLAY_CONV tsarto_CONV))) 102 (Count.apply (RAND_CONV (FAPPLY_CONV tsarto_CONV)) (* 178 prim infs *) THENC 103 Count.apply (IN_CONV tsarto_CONV) (* 221 prim infs *)) testNic2 114 Count.apply (TC_CONV TSAR_EQ_CONV) ``(FMAP_TO_RELN ^RomHasse)^+``; 123 (Count.apply (RAND_CONV (FAPPLY_CONV TSAR_EQ_CONV)) (* 66 prim infs *) THENC 124 Count.apply (IN_CONV TSAR_EQ_CONV) (* 473 prim infs *)) testNic2
|
H A D | flookupLib.sml | 302 Count.apply EVAL ``FLOOKUP (FEMPTY |+ (a, 1)) a`` 304 Count.apply EVAL ``FLOOKUP ^(mk_fmap fempty_tm 0 1000) 999`` 306 Count.apply EVAL ``FLOOKUP gen_fmap_0 44`` 307 Count.apply EVAL ``FLOOKUP (gen_fmap_0 |+ (1000, 1000)) 44`` 308 Count.apply EVAL ``FLOOKUP (gen_fmap_0 |+ (44, 45)) 44`` 309 Count.apply EVAL ``FLOOKUP gen_fmap_1 99`` 310 Count.apply EVAL ``FLOOKUP gen_fmap_9 99`` 311 Count.apply EVAL ``FLOOKUP gen_fmap_9 901`` 312 Count.apply EVAL ``FLOOKUP gen_fmap_9 801`` 339 val d2_conv = Count.apply FLOOKUP_DEFN_CON [all...] |
/seL4-l4v-master/HOL4/src/proofman/ |
H A D | History.sig | 8 val apply : ('a -> 'a) -> 'a history -> 'a history value
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | SatisfySimps.sml | 12 apply=SATISFY_CONV o get_db o #context,
|
/seL4-l4v-master/HOL4/examples/formal-languages/context-free/ |
H A D | pegML.sml | 63 empty v => apply G k input (SOME v::results) 65 [] => apply G fk input results 66 | h::t => apply G k t (SOME (tf h)::results)) 68 [] => apply G fk input results 69 | x::xs => if x = t then apply G k xs (SOME v::results) 70 else apply G fk input results) 87 and apply G (k:(''i,'v)kont) input (results:'v option list) = function 92 | applyf(f, k) => apply G k input (f results) 93 | returnTo(i,r,k) => apply G k i r 96 | poplist(f,k) => apply [all...] |
/seL4-l4v-master/HOL4/examples/pgcl/examples/ |
H A D | verification.sml | 36 val prob_then_demon = Count.apply prove 46 val demon_then_prob = Count.apply prove 56 val partial_demon_then_prob = Count.apply prove 71 val wp_loop = Count.apply prove 88 val wlp_loop = Count.apply prove 136 val partial_monty_hall = Count.apply prove 147 val monty_hall = Count.apply prove 177 val lurch_once = Count.apply prove 189 val lurch_once_home = Count.apply prove 198 val lurch_once_home' = Count.apply prov [all...] |
/seL4-l4v-master/HOL4/src/emit/ |
H A D | ConstMapML.sig | 13 val apply : term -> bool * string * string * hol_type value 16 (* [apply] peforms a lookup and returns the most specific match. Thus,
|