/seL4-l4v-10.1.1/isabelle/Admin/lib/Tools/ |
H A D | components_checksum | 39 UPDATE="" 47 UPDATE=true 57 [ -n "$UPDATE" ] || [ -n "$CHECK" ] || usage 77 [ -n "$UPDATE" ] && mv "$CHECKSUM_TMP" "$CHECKSUM_FILE"
|
/seL4-l4v-10.1.1/l4v/isabelle/Admin/lib/Tools/ |
H A D | components_checksum | 39 UPDATE="" 47 UPDATE=true 57 [ -n "$UPDATE" ] || [ -n "$CHECK" ] || usage 77 [ -n "$UPDATE" ] && mv "$CHECKSUM_TMP" "$CHECKSUM_FILE"
|
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/ |
H A D | reductionScript.sml | 333 (!l m. Ro (UPDATE o1 l m) (UPDATE o2 l m)) /\ 341 (!m1 m2. Rm m1 m2 ==> (!o' l. Ro (UPDATE o' l m1) (UPDATE o' l m2)) 430 (^RED1_obj R (UPDATE o1 l m) (UPDATE o2 l m))) /\ 435 (^RED1_obj R (UPDATE a l m1) (UPDATE a l m2))) /\ 486 P_0 R o1 o2 ==> P_0 R (UPDATE o1 l m) (UPDATE o [all...] |
H A D | semanticsScript.sml | 392 (* INVOKE (OBJ d) l or UPDATE (OBJ d) l m *) 408 (^SIGMA_R (UPDATE (OBJ d) l m) (update (OBJ d) l m)) 470 (!o1 l o2. SIGMA_R (UPDATE o1 l m) o2 = 574 (^REDL_obj (UPDATE o1 l m1) (UPDATE o2 l m2))) /\ 614 (^REDL_obj (UPDATE (OBJ d1) l m1) (update (OBJ d2) l m2))) 647 P_0 (UPDATE o1 l m1) (UPDATE o2 l m2)) /\ 652 P_0 (UPDATE (OBJ d1) l m1) (update (OBJ d2) l m2)) /\ 772 P_0 (UPDATE o [all...] |
H A D | liftScript.sml | 1309 {def_name="UPDATE_def", fname="UPDATE", 1664 obj_Prop o' /\ method_Prop m ==> (!l. obj_Prop (UPDATE o' l m))) /\ 1739 obj_Prop o' /\ method_Prop m ==> (!l. obj_Prop (UPDATE o' l m))) /\
|
/seL4-l4v-10.1.1/HOL4/src/num/ |
H A D | numLib.sml | 9 (* UPDATE : October'94 bugfix to num_EQ_CONV (KLS;bugfix from tfm)*) 10 (* UPDATE : January'99 fix to use "Norrish" numerals (MN) *) 11 (* UPDATE : August'99 to incorporate num_CONV and INDUCT_TAC *) 12 (* UPDATE : Nov'99 to incorporate main entrypoints from *)
|
/seL4-l4v-10.1.1/HOL4/src/combin/ |
H A D | combinSyntax.sml | 15 val update_tm = prim_mk_const{Name="UPDATE", Thy="combin"};
|
H A D | combinScript.sml | 30 `UPDATE a b = \f c. if a = c then b else f c`); 34 val _ = overload_on("=+", ``UPDATE``);
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
H A D | PKGS.sml | 1004 ("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS" , "ACL2" , "COMMON-LISP"), 1006 ("UPDATE-INSTANCE-FOR-REDEFINED-CLASS" , "ACL2" , "COMMON-LISP"), 1916 ("LEN-UPDATE-NTH" , "ACL2-USER" , "ACL2"), 2121 ("NTH-UPDATE-NTH" , "ACL2-USER" , "ACL2"), 2586 ("STATE-P1-UPDATE-MAIN-TIMER" , "ACL2-USER" , "ACL2"), 2587 ("STATE-P1-UPDATE-NTH-2-WORLD" , "ACL2-USER" , "ACL2"), 2728 ("TRUE-LISTP-UPDATE-NTH" , "ACL2-USER" , "ACL2"), 2772 ("UPDATE-32-BIT-INTEGER-STACK" , "ACL2-USER" , "ACL2"), 2773 ("UPDATE-ACL2-ORACLE" , "ACL2-USER" , "ACL2"), 2774 ("UPDATE [all...] |
H A D | hol_defaxiomsScript.sml | 2824 [oracles: DEFUN ACL2::UPDATE-NTH, DISK_THM] [axioms: ] [] 2831 [oracles: DEFUN ACL2::UPDATE-NTH-ARRAY] [axioms: ] [] 2873 [oracles: DEFUN ACL2::UPDATE-OPEN-INPUT-CHANNELS, DISK_THM] [axioms: ] 2883 [oracles: DEFUN ACL2::UPDATE-OPEN-OUTPUT-CHANNELS, DISK_THM] [axioms: ] 2893 [oracles: DEFUN ACL2::UPDATE-GLOBAL-TABLE, DISK_THM] [axioms: ] [] 2903 [oracles: DEFUN ACL2::UPDATE-T-STACK, DISK_THM] [axioms: ] [] 2913 [oracles: DEFUN ACL2::UPDATE-32-BIT-INTEGER-STACK, DISK_THM] [axioms: ] 2923 [oracles: DEFUN ACL2::UPDATE-BIG-CLOCK-ENTRY, DISK_THM] [axioms: ] [] 2933 [oracles: DEFUN ACL2::UPDATE-IDATES, DISK_THM] [axioms: ] [] 2943 [oracles: DEFUN ACL2::UPDATE [all...] |
H A D | m1_story.sml | 78 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "UPDATE-NTH") ( 1200 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "NTH-UPDATE-NTH") (mkpair ( 1208 mksym "M1" "UPDATE-NTH") (mkpair (mksym "M1" "J") (mkpair (mksym "M1" "V") ( 1219 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "UPDATE-NTH-UPDATE-NTH-1") ( 1231 "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "UPDATE-NTH") (mkpair ( 1233 "UPDATE-NTH") (mkpair (mksym "M1" "J") (mkpair (mksym "M1" "W") (mkpair ( 1235 "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "M1" "UPDATE-NTH") (mkpair ( 1237 "UPDATE-NTH") (mkpair (mksym "M1" "I") (mkpair (mksym "M1" "V") (mkpair ( 1243 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "UPDATE [all...] |
H A D | problem_set_1_answers.sml | 194 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "UPDATE-NTH") ( 203 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "UPDATE-NTH") (
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/ |
H A D | PKGS.sml | 963 ("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS" , "ACL2" , "COMMON-LISP"), 965 ("UPDATE-INSTANCE-FOR-REDEFINED-CLASS" , "ACL2" , "COMMON-LISP"), 1875 ("LEN-UPDATE-NTH" , "ACL2-USER" , "ACL2"), 2080 ("NTH-UPDATE-NTH" , "ACL2-USER" , "ACL2"), 2545 ("STATE-P1-UPDATE-MAIN-TIMER" , "ACL2-USER" , "ACL2"), 2546 ("STATE-P1-UPDATE-NTH-2-WORLD" , "ACL2-USER" , "ACL2"), 2687 ("TRUE-LISTP-UPDATE-NTH" , "ACL2-USER" , "ACL2"), 2731 ("UPDATE-32-BIT-INTEGER-STACK" , "ACL2-USER" , "ACL2"), 2732 ("UPDATE-ACL2-ORACLE" , "ACL2-USER" , "ACL2"), 2733 ("UPDATE [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | kpa-v2-9-3.ml | 373 ("LEN-UPDATE-NTH", "ACL2-USER", "ACL2"), 431 ("NTH-UPDATE-NTH", "ACL2-USER", "ACL2"), 624 ("STATE-P1-UPDATE-MAIN-TIMER", "ACL2-USER", "ACL2"), 625 ("STATE-P1-UPDATE-NTH-2-WORLD", "ACL2-USER", "ACL2"), 692 ("TRUE-LISTP-UPDATE-NTH", "ACL2-USER", "ACL2"), 710 ("UPDATE-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"), 711 ("UPDATE-BIG-CLOCK-ENTRY", "ACL2-USER", "ACL2"), 712 ("UPDATE-FILE-CLOCK", "ACL2-USER", "ACL2"), 713 ("UPDATE-GLOBAL-TABLE", "ACL2-USER", "ACL2"), 714 ("UPDATE [all...] |
H A D | acl2_packageScript.sml | 484 ("LEN-UPDATE-NTH", "ACL2-USER", "ACL2"), 542 ("NTH-UPDATE-NTH", "ACL2-USER", "ACL2"), 735 ("STATE-P1-UPDATE-MAIN-TIMER", "ACL2-USER", "ACL2"), 736 ("STATE-P1-UPDATE-NTH-2-WORLD", "ACL2-USER", "ACL2"), 803 ("TRUE-LISTP-UPDATE-NTH", "ACL2-USER", "ACL2"), 821 ("UPDATE-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"), 822 ("UPDATE-BIG-CLOCK-ENTRY", "ACL2-USER", "ACL2"), 823 ("UPDATE-FILE-CLOCK", "ACL2-USER", "ACL2"), 824 ("UPDATE-GLOBAL-TABLE", "ACL2-USER", "ACL2"), 825 ("UPDATE [all...] |
H A D | hol_defaxiomsScript.sml | 2782 [oracles: DEFUN ACL2::UPDATE-NTH, DISK_THM] [axioms: ] [] 2789 [oracles: DEFUN ACL2::UPDATE-NTH-ARRAY] [axioms: ] [] 2831 [oracles: DEFUN ACL2::UPDATE-OPEN-INPUT-CHANNELS, DISK_THM] [axioms: ] 2841 [oracles: DEFUN ACL2::UPDATE-OPEN-OUTPUT-CHANNELS, DISK_THM] [axioms: ] 2851 [oracles: DEFUN ACL2::UPDATE-GLOBAL-TABLE, DISK_THM] [axioms: ] [] 2861 [oracles: DEFUN ACL2::UPDATE-T-STACK, DISK_THM] [axioms: ] [] 2871 [oracles: DEFUN ACL2::UPDATE-32-BIT-INTEGER-STACK, DISK_THM] [axioms: ] 2881 [oracles: DEFUN ACL2::UPDATE-BIG-CLOCK-ENTRY, DISK_THM] [axioms: ] [] 2891 [oracles: DEFUN ACL2::UPDATE-IDATES, DISK_THM] [axioms: ] [] 2901 [oracles: DEFUN ACL2::UPDATE [all...] |
H A D | defaxioms.lisp.trans.ml | 4897 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "UPDATE-NTH") ( 4906 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "UPDATE-NTH") (mkpair ( 4916 "UPDATE-NTH-ARRAY") (mkpair (mkpair (mksym "ACL2" "J") (mkpair (mksym "ACL2" 4918 "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "UPDATE-NTH") (mkpair ( 4919 mksym "ACL2" "J") (mkpair (mkpair (mksym "ACL2" "UPDATE-NTH") (mkpair (mksym 5009 "UPDATE-OPEN-INPUT-CHANNELS") (mkpair (mkpair (mksym "ACL2" "X") (mkpair ( 5011 "ACL2" "UPDATE-NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 5026 "UPDATE-OPEN-OUTPUT-CHANNELS") (mkpair (mkpair (mksym "ACL2" "X") (mkpair ( 5028 "ACL2" "UPDATE-NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 5043 "UPDATE [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | acl2_packageScript.sml | 484 ("LEN-UPDATE-NTH", "ACL2-USER", "ACL2"), 542 ("NTH-UPDATE-NTH", "ACL2-USER", "ACL2"), 735 ("STATE-P1-UPDATE-MAIN-TIMER", "ACL2-USER", "ACL2"), 736 ("STATE-P1-UPDATE-NTH-2-WORLD", "ACL2-USER", "ACL2"), 803 ("TRUE-LISTP-UPDATE-NTH", "ACL2-USER", "ACL2"), 821 ("UPDATE-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"), 822 ("UPDATE-BIG-CLOCK-ENTRY", "ACL2-USER", "ACL2"), 823 ("UPDATE-FILE-CLOCK", "ACL2-USER", "ACL2"), 824 ("UPDATE-GLOBAL-TABLE", "ACL2-USER", "ACL2"), 825 ("UPDATE [all...] |
H A D | hol_defaxiomsScript.sml | 2786 [oracles: DEFUN ACL2::UPDATE-NTH, DISK_THM] [axioms: ] [] 2793 [oracles: DEFUN ACL2::UPDATE-NTH-ARRAY] [axioms: ] [] 2835 [oracles: DEFUN ACL2::UPDATE-OPEN-INPUT-CHANNELS, DISK_THM] [axioms: ] 2845 [oracles: DEFUN ACL2::UPDATE-OPEN-OUTPUT-CHANNELS, DISK_THM] [axioms: ] 2855 [oracles: DEFUN ACL2::UPDATE-GLOBAL-TABLE, DISK_THM] [axioms: ] [] 2865 [oracles: DEFUN ACL2::UPDATE-T-STACK, DISK_THM] [axioms: ] [] 2875 [oracles: DEFUN ACL2::UPDATE-32-BIT-INTEGER-STACK, DISK_THM] [axioms: ] 2885 [oracles: DEFUN ACL2::UPDATE-BIG-CLOCK-ENTRY, DISK_THM] [axioms: ] [] 2895 [oracles: DEFUN ACL2::UPDATE-IDATES, DISK_THM] [axioms: ] [] 2905 [oracles: DEFUN ACL2::UPDATE [all...] |
H A D | records.ml | 337 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "UPDATE-MACRO") ( 342 "ACL2" "UPDATE-MACRO") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/gold/ |
H A D | m1_story.sml | 78 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "UPDATE-NTH") ( 1200 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "NTH-UPDATE-NTH") (mkpair ( 1208 mksym "M1" "UPDATE-NTH") (mkpair (mksym "M1" "J") (mkpair (mksym "M1" "V") ( 1219 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "UPDATE-NTH-UPDATE-NTH-1") ( 1231 "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "UPDATE-NTH") (mkpair ( 1233 "UPDATE-NTH") (mkpair (mksym "M1" "J") (mkpair (mksym "M1" "W") (mkpair ( 1235 "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "M1" "UPDATE-NTH") (mkpair ( 1237 "UPDATE-NTH") (mkpair (mksym "M1" "I") (mkpair (mksym "M1" "V") (mkpair ( 1243 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "UPDATE [all...] |
H A D | problem_set_1_answers.sml | 194 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "UPDATE-NTH") ( 203 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "UPDATE-NTH") (
|
H A D | records.sml | 332 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "UPDATE-MACRO") ( 337 "ACL2" "UPDATE-MACRO") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
|
/seL4-l4v-10.1.1/HOL4/src/Boolify/test/ |
H A D | datatypes.sml | 264 | UPDATE of obj => string => method ; 287 /\ (FV_obj (UPDATE o1 l m) = APPEND (FV_obj o1) (FV_method m))
|
/seL4-l4v-10.1.1/HOL4/src/0/ |
H A D | Type.sml | 7 (* UPDATE : October 94. Type signature implementation moved from *)
|