Update Isabelle and HOL snapshots

2 files changed, 36 insertions, 36 deletions

diff --git a/snapshots/hol4/sail/lib/hol/sail2_operators_bitlistsScript.sml b/snapshots/hol4/sail/lib/hol/sail2_operators_bitlistsScript.sml
index da349336..88c06749 100644
--- a/snapshots/hol4/sail/lib/hol/sail2_operators_bitlistsScript.sml
+++ b/snapshots/hol4/sail/lib/hol/sail2_operators_bitlistsScript.sml
@@ -328,42 +328,42 @@ val _ = Define `
      instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) T))`;
 
 
-(*val add_vec_int      : list bitU -> integer -> list bitU*)
-(*val sub_vec_int      : list bitU -> integer -> list bitU*)
-(*val mult_vec_int     : list bitU -> integer -> list bitU*)
+(*val add_vec_int       : list bitU -> integer -> list bitU*)
+(*val sub_vec_int       : list bitU -> integer -> list bitU*)
+(*val mult_vec_int      : list bitU -> integer -> list bitU*)
 val _ = Define `
- ((add_vec_int0:(bitU)list -> int ->(bitU)list)  l r=  (arith_op_bv_int 
+ ((add_vec_int0:(bitU)list -> int ->(bitU)list)   l r=  (arith_op_bv_int 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (+) T l r))`;
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (+) F l r))`;
 
 val _ = Define `
- ((sub_vec_int0:(bitU)list -> int ->(bitU)list)  l r=  (arith_op_bv_int 
+ ((sub_vec_int0:(bitU)list -> int ->(bitU)list)   l r=  (arith_op_bv_int 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (-) T l r))`;
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (-) F l r))`;
 
 val _ = Define `
- ((mult_vec_int0:(bitU)list -> int ->(bitU)list) l r=  (arith_op_double_bl 
+ ((mult_vec_int0:(bitU)list -> int ->(bitU)list)  l r=  (arith_op_double_bl 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) T l (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH l)) r))))`;
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) F l (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH l)) r))))`;
 
 
-(*val add_int_vec      : integer -> list bitU -> list bitU*)
-(*val sub_int_vec      : integer -> list bitU -> list bitU*)
-(*val mult_int_vec     : integer -> list bitU -> list bitU*)
+(*val add_int_vec       : integer -> list bitU -> list bitU*)
+(*val sub_int_vec       : integer -> list bitU -> list bitU*)
+(*val mult_int_vec      : integer -> list bitU -> list bitU*)
 val _ = Define `
- ((add_int_vec0:int ->(bitU)list ->(bitU)list)  l r=  (arith_op_int_bv 
+ ((add_int_vec0:int ->(bitU)list ->(bitU)list)   l r=  (arith_op_int_bv 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (+) T l r))`;
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (+) F l r))`;
 
 val _ = Define `
- ((sub_int_vec0:int ->(bitU)list ->(bitU)list)  l r=  (arith_op_int_bv 
+ ((sub_int_vec0:int ->(bitU)list ->(bitU)list)   l r=  (arith_op_int_bv 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (-) T l r))`;
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (-) F l r))`;
 
 val _ = Define `
- ((mult_int_vec0:int ->(bitU)list ->(bitU)list) l r=  (arith_op_double_bl 
+ ((mult_int_vec0:int ->(bitU)list ->(bitU)list)  l r=  (arith_op_double_bl 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) T (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH r)) l)) r))`;
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) F (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH r)) l)) r))`;
 
 
 (*val add_vec_bit      : list bitU -> bitU -> list bitU*)
diff --git a/snapshots/hol4/sail/lib/hol/sail2_operators_mwordsScript.sml b/snapshots/hol4/sail/lib/hol/sail2_operators_mwordsScript.sml
index 9276cfef..5b0e7723 100644
--- a/snapshots/hol4/sail/lib/hol/sail2_operators_mwordsScript.sml
+++ b/snapshots/hol4/sail/lib/hol/sail2_operators_mwordsScript.sml
@@ -278,36 +278,36 @@ val _ = Define `
  ((mults_vec:'a words$word -> 'a words$word -> 'b words$word) l r=  (integer_word$i2w ((int_of_mword T (words$sw2sw l :  'b words$word)) * (int_of_mword T (words$sw2sw r :  'b words$word)))))`;
 
 
-(*val add_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*)
-(*val sub_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*)
-(*val mult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b*)
+(*val add_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*)
+(*val sub_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*)
+(*val mult_vec_int  : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b*)
 val _ = Define `
- ((add_vec_int:'a words$word -> int -> 'a words$word)  l r=  (arith_op_bv_int 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict (+)   T  l r))`;
+ ((add_vec_int:'a words$word -> int -> 'a words$word)   l r=  (arith_op_bv_int 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict (+)   F l r))`;
 
 val _ = Define `
- ((sub_vec_int:'a words$word -> int -> 'a words$word)  l r=  (arith_op_bv_int 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict (-) T  l r))`;
+ ((sub_vec_int:'a words$word -> int -> 'a words$word)   l r=  (arith_op_bv_int 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict (-) F l r))`;
 
 val _ = Define `
- ((mult_vec_int:'a words$word -> int -> 'b words$word) l r=  (arith_op_bv_int 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict ( * )  T  (words$sw2sw l :  'b words$word) r))`;
+ ((mult_vec_int:'a words$word -> int -> 'b words$word)  l r=  (arith_op_bv_int 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict ( * )  F (words$w2w l :  'b words$word) r))`;
 
 
-(*val add_int_vec  : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*)
-(*val sub_int_vec  : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*)
-(*val mult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b*)
+(*val add_int_vec   : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*)
+(*val sub_int_vec   : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*)
+(*val mult_int_vec  : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b*)
 val _ = Define `
- ((add_int_vec:int -> 'a words$word -> 'a words$word)  l r=  (arith_op_int_bv 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict (+)   T  l r))`;
+ ((add_int_vec:int -> 'a words$word -> 'a words$word)   l r=  (arith_op_int_bv 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict (+)   F l r))`;
 
 val _ = Define `
- ((sub_int_vec:int -> 'a words$word -> 'a words$word)  l r=  (arith_op_int_bv 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict (-) T  l r))`;
+ ((sub_int_vec:int -> 'a words$word -> 'a words$word)   l r=  (arith_op_int_bv 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict (-) F l r))`;
 
 val _ = Define `
- ((mult_int_vec:int -> 'a words$word -> 'b words$word) l r=  (arith_op_int_bv 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict ( * )  T  l (words$sw2sw r :  'b words$word)))`;
+ ((mult_int_vec:int -> 'a words$word -> 'b words$word)  l r=  (arith_op_int_bv 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict ( * )  F l (words$w2w r :  'b words$word)))`;
 
 
 (*val add_vec_bool  : forall 'a. Size 'a => mword 'a -> bool -> mword 'a*)