Searched refs:undo (Results 1 - 19 of 19) sorted by relevance
| /seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
| H A D | VarOrder.h | 49 inline void undo(Var x); // Called when variable is unassigned and may be selected again.
68 void VarOrder::undo(Var x) function in class:VarOrder
|
| H A D | Solver.C | 220 order.undo(x); }
|
| /seL4-l4v-10.1.1/HOL4/src/proofman/ |
| H A D | History.sig | 13 val undo : 'a history -> 'a history value
|
| H A D | History.sml | 3 (* "project"), write (via "apply"), and undo. *)
35 fun undo (HISTORY{past=[], ...}) = raise CANT_BACKUP_ANYMORE function
36 | undo (HISTORY{past=h::rst, limit, orig,save_points,...}) =
|
| H A D | Manager.sml | 9 (* Add a notion of undo to the two kinds of proof manager *)
69 fun backup (GOALSTACK s) = GOALSTACK(undo s)
70 | backup (GOALTREE t) = GOALTREE(undo t);
|
| H A D | goalStack.sml | 2 (* Goalstacks, with no idea of undo. *)
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | match_goal.sig | 55 - if it fails: undo abbreviations, backtrack
56 - if it succeeds: undo abbreviations, done
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/poly/ |
| H A D | holfoot_command_line.sml | 66 val s = " b undo\n";
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
| H A D | holfootLib.sml | 1723 (*undo resorting*)
1889 (*undo resorting*)
1962 (*undo resorting*)
2047 (*undo resorting*)
2122 (*undo resorting*)
2190 (*undo resorting*)
|
| /seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
| H A D | Z3_ProofParser.sml | 363 (* undo look-ahead of 2 tokens *)
|
| H A D | Z3_ProofReplay.sml | 846 (* cache 'thm', instantiate to undo 'generalize_ite' *)
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Intro/document/ |
| H A D | getting.tex | 436 \item[\ttindex{undo}(); ]
438 undone. Do not omit the parentheses; typing {\tt\ \ undo;\ \ } merely
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Intro/document/ |
| H A D | getting.tex | 436 \item[\ttindex{undo}(); ]
438 undone. Do not omit the parentheses; typing {\tt\ \ undo;\ \ } merely
|
| /seL4-l4v-10.1.1/HOL4/Manual/Interaction/ |
| H A D | HOL-interaction.tex | 153 You can undo the effect of the applied tactic by pressing {\tt M-h b}. Press {\tt M-h p} to view the current goal.
|
| /seL4-l4v-10.1.1/seL4/manual/parts/ |
| H A D | threads.tex | 414 invocation and a second invocation will undo the previous one. The link also means that
|
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/ |
| H A D | euclid.tex | 541 fin dall'inizio. Di conseguenza facciamo un backup. Dovremo fare un backup (undo) tre volte.
1755 \ml{bossLib} e ha toccato questioni che includono la selezione degli strumenti, l'undo,
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
| H A D | configure | 1534 --enable-silent-rules less verbose build output (undo: "make V=1")
1535 --disable-silent-rules verbose build output (undo: "make V=0")
|
| H A D | texinfo.tex | 3896 % undo it ourselves.
|
| /seL4-l4v-10.1.1/HOL4/polyml/ |
| H A D | configure | 1495 --enable-silent-rules less verbose build output (undo: "make V=1")
1496 --disable-silent-rules verbose build output (undo: "make V=0")
|
Completed in 364 milliseconds