src/HOL/Import/Generate-HOL/GenHOL4Prob.thy
changeset 17566 484ff733f29c
parent 16417 9bc16273c2d4
child 41589 bbd861837ebc
equal deleted inserted replaced
17565:7322f37d3344 17566:484ff733f29c
     7 
     7 
     8 import_segment "hol4";
     8 import_segment "hol4";
     9 
     9 
    10 setup_dump "../HOL" "HOL4Prob";
    10 setup_dump "../HOL" "HOL4Prob";
    11 
    11 
    12 append_dump "theory HOL4Prob = HOL4Real:";
    12 append_dump "theory HOL4Prob imports HOL4Real begin";
    13 
    13 
    14 import_theory prob_extra;
    14 import_theory prob_extra;
    15 
    15 
    16 const_moves
    16 const_moves
    17   COMPL > GenHOL4Base.pred_set.COMPL;
    17   COMPL > GenHOL4Base.pred_set.COMPL;