src/HOL/Import/patches/patch1
changeset 81924 61b711122061
parent 81919 f4cd3e679096
child 81931 3c888cd24351
equal deleted inserted replaced
81923:02b4ae06974d 81924:61b711122061
    16 +  close_out oc
    16 +  close_out oc
    17 +;;
    17 +;;
    18 +dump_theorems ();;
    18 +dump_theorems ();;
    19 --- hol-light/stage1.ml	1970-01-01 01:00:00.000000000 +0100
    19 --- hol-light/stage1.ml	1970-01-01 01:00:00.000000000 +0100
    20 +++ hol-light-patched/stage1.ml	2025-01-18 11:12:11.185279392 +0100
    20 +++ hol-light-patched/stage1.ml	2025-01-18 11:12:11.185279392 +0100
    21 @@ -0,0 +1,4 @@
    21 @@ -0,0 +1,5 @@
    22 +#use "hol.ml";;
    22 +#use "hol.ml";;
       
    23 +(*LOAD MORE*)
    23 +#use "update_database.ml";;
    24 +#use "update_database.ml";;
    24 +#use "statements.ml";;
    25 +#use "statements.ml";;
    25 +exit 0;;
    26 +exit 0;;
    26 --- hol-light/stage2.ml	1970-01-01 01:00:00.000000000 +0100
    27 --- hol-light/stage2.ml	1970-01-01 01:00:00.000000000 +0100
    27 +++ hol-light-patched/stage2.ml	2025-01-18 11:12:11.384276293 +0100
    28 +++ hol-light-patched/stage2.ml	2025-01-18 11:12:11.384276293 +0100
    28 @@ -0,0 +1,3 @@
    29 @@ -0,0 +1,4 @@
    29 +#use "hol.ml";;
    30 +#use "hol.ml";;
       
    31 +(*LOAD MORE*)
    30 +stop_recording ();;
    32 +stop_recording ();;
    31 +exit 0;;
    33 +exit 0;;