src/Tools/isac/Knowledge/InsSort.thy
changeset 55359 73dc85c025ab
parent 55339 cccd24e959ba
child 55363 d78bc1342183
equal deleted inserted replaced
55358:b1f0389ca11f 55359:73dc85c025ab
    75   [("#Given" ,["unsorted u_"]),
    75   [("#Given" ,["unsorted u_"]),
    76    ("#Find"  ,["sorted s_"])
    76    ("#Find"  ,["sorted s_"])
    77   ],
    77   ],
    78   []));
    78   []));
    79 *}
    79 *}
    80 setup {* KEStore_Elems.store_pbts
    80 setup {* KEStore_Elems.add_pbts
    81   [(prep_pbt @{theory "InsSort"}
    81   [(prep_pbt @{theory "InsSort"}
    82       (["functional"]:pblID,
    82       (["functional"]:pblID,
    83         [("#Given" ,["unsorted u_"]), ("#Find"  ,["sorted s_"])], [])),
    83         [("#Given" ,["unsorted u_"]), ("#Find"  ,["sorted s_"])], [])),
    84     (prep_pbt @{theory "InsSort"}
    84     (prep_pbt @{theory "InsSort"}
    85       (["inssort","functional"]:pblID,
    85       (["inssort","functional"]:pblID,