| /seL4-l4v-10.1.1/HOL4/Manual/Tutorial/ |
| H A D | logic.tex | 1250 \noindent \ml{GEN\_TAC} strips off one quantifier;
1251 \ml{REPEAT\ GEN\_TAC} strips off all quantifiers:
1398 \item{\bf Summary:} Strips off one universal quantifier.
1414 {\small\verb|REPEAT GEN_TAC|} strips off all
1429 \item {\bf Uses:} To finish a goal off when it is clear that it is a
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
| H A D | mechReasoning.sml | 199 fun conv (IRSyntax.MEM (b, off)) = SIM_MEM_CONV
380 | clean_pair (IRSyntax.MEM (r, off)) = IRSyntax.MEM (r, off)
|
| /seL4-l4v-10.1.1/HOL4/Manual/Description/ |
| H A D | holCheck.tex | 166 This section describes the usage of \hc{} in more detail. As a running example we will take the children's game of tic-tac-toe or noughts-and-crosses, usually played on a 3-by-3 grid. For simplicity and to keep the formulas under consideration manageable, we consider the trivial 1-by-1 variant. Thus, the grid starts off empty, the player to go first makes a move and immediately wins, ending the game.
560 \hc{} implements a fully automatic abstraction refinement framework that is invisible to the user. A simple heuristic analysis is used to decide whether or not to apply abstraction for a given property. Sometimes the abstraction may make things worse. If \hc{} appears to be taking overly long on a property, the user may try redoing the check, after turning off abstraction. This can be done by calling \texttt{set\_flag\_abs} on the model. Turning abstraction on and off on a per-property basis is not supported yet.
|
| H A D | QuantHeuristics.tex | 219 A special (degenerated) use of the framework, is turning guess search off completely and
|
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
| H A D | holCheck.tex | 166 This section describes the usage of \hc{} in more detail. As a running example we will take the children's game of tic-tac-toe or noughts-and-crosses, usually played on a 3-by-3 grid. For simplicity and to keep the formulas under consideration manageable, we consider the trivial 1-by-1 variant. Thus, the grid starts off empty, the player to go first makes a move and immediately wins, ending the game.
560 \hc{} implements a fully automatic abstraction refinement framework that is invisible to the user. A simple heuristic analysis is used to decide whether or not to apply abstraction for a given property. Sometimes the abstraction may make things worse. If \hc{} appears to be taking overly long on a property, the user may try redoing the check, after turning off abstraction. This can be done by calling \texttt{set\_flag\_abs} on the model. Turning abstraction on and off on a per-property basis is not supported yet.
|
| H A D | QuantHeuristics.tex | 219 A special (degenerated) use of the framework, is turning guess search off completely and
|
| /seL4-l4v-10.1.1/HOL4/src/IndDef/ |
| H A D | IndDefRules.sml | 210 (* tactic applies GTAC x as many times as required. It then strips off *)
|
| H A D | InductiveDefinition.sml | 61 (* Strip off exactly n arguments from combination. *)
|
| /seL4-l4v-10.1.1/HOL4/src/enumfset/ |
| H A D | tcScript.sml | 93 (* Outer ^| s is meant just to trim off (x,x) pairs for x NOTIN s, and we
|
| /seL4-l4v-10.1.1/HOL4/src/num/termination/ |
| H A D | TotalDefn.sml | 667 (* Turn off printing of messages by the HOL system for the duration of the *)
|
| /seL4-l4v-10.1.1/HOL4/src/portableML/mosml/ |
| H A D | Arbnumcore.sml | 40 | less1 [x] = if x = 0 then raise Fail "Can't take one off zero"
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/LTL/ |
| H A D | LTLScript.sml | 15 quietdec := true; (* Switch off output *)
|
| /seL4-l4v-10.1.1/HOL4/polyml/basis/ |
| H A D | Int.sml | 128 value is long. Instead of reducing it by the radix each time we take off
|
| H A D | TopLevelPolyML.sml | 1542 (* Turn off interrupts for the interface thread. *)
1586 print "-q Suppress the start-up message and turn off printing of results\n";
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
| H A D | CommonDialog.sml | 660 (* Most of the fields are unchanged so we're better off extracting
693 (* Mask off the template flags. *)
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Prim_rec.sml | 99 (* here we rely on the assumption that the combs we split off were the
527 (* tactic applies GTAC x as many times as required. It then strips off *)
|
| /seL4-l4v-10.1.1/HOL4/examples/diningcryptos/ |
| H A D | formalizeUseful.sml | 778 fun REPEATC_CUTOFF 0 _ _ = raise ERR "REPEATC_CUTOFF" "cut-off reached"
|
| H A D | subtypeUseful.sml | 783 fun REPEATC_CUTOFF 0 _ _ = raise ERR "REPEATC_CUTOFF" "cut-off reached"
|
| /seL4-l4v-10.1.1/HOL4/src/coalgebras/ |
| H A D | lbtreeScript.sml | 570 discarded from the head of the list, or as a Nd is pulled off,
|
| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | OmegaMath.sml | 751 Perform cond_removal0 on all of t's disjunctions, not being put off
|
| /seL4-l4v-10.1.1/HOL4/src/quotient/src/ |
| H A D | quotient.sml | 2489 (* The function get_higher_wf_base strips off all quotient conditions from
2491 strips off any remaining antecedent, returning the consequent as the "base".
2529 (* The function get_higher_eq_base strips off all quotient conditions from
2531 strips off the right hand side if it is an equality, and returns the
|
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
| H A D | Holmake.sml | 178 finishes off; this parameter is called when all of the necessary
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/ |
| H A D | x86_decoderScript.sml | 119 else (* normal cases, just need to read off the correct displacement *)
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
| H A D | x64_decoderScript.sml | 157 else (* normal cases, just need to read off the correct displacement *)
|
| /seL4-l4v-10.1.1/HOL4/examples/miller/useful/ |
| H A D | HurdUseful.sml | 720 fun REPEATC_CUTOFF 0 _ _ = raise ERR "REPEATC_CUTOFF" "cut-off reached"
|