1326 fun rewrite_proof_notypes rews = rewrite_prf fst rews; |
1326 fun rewrite_proof_notypes rews = rewrite_prf fst rews; |
1327 |
1327 |
1328 |
1328 |
1329 (**** theory data ****) |
1329 (**** theory data ****) |
1330 |
1330 |
1331 structure ProofData = Theory_Data |
1331 structure Data = Theory_Data |
1332 ( |
1332 ( |
1333 type T = |
1333 type T = |
1334 (stamp * (proof * proof)) list * |
1334 (stamp * (proof * proof)) list * |
1335 (stamp * (typ list -> proof -> (proof * proof) option)) list; |
1335 (stamp * (typ list -> proof -> (proof * proof) option)) list; |
1336 |
1336 |
1339 fun merge ((rules1, procs1), (rules2, procs2)) : T = |
1339 fun merge ((rules1, procs1), (rules2, procs2)) : T = |
1340 (AList.merge (op =) (K true) (rules1, rules2), |
1340 (AList.merge (op =) (K true) (rules1, rules2), |
1341 AList.merge (op =) (K true) (procs1, procs2)); |
1341 AList.merge (op =) (K true) (procs1, procs2)); |
1342 ); |
1342 ); |
1343 |
1343 |
1344 fun get_data thy = let val (rules, procs) = ProofData.get thy in (map #2 rules, map #2 procs) end; |
1344 fun get_data thy = let val (rules, procs) = Data.get thy in (map #2 rules, map #2 procs) end; |
1345 fun rew_proof thy = rewrite_prf fst (get_data thy); |
1345 fun rew_proof thy = rewrite_prf fst (get_data thy); |
1346 |
1346 |
1347 fun add_prf_rrule r = (ProofData.map o apfst) (cons (stamp (), r)); |
1347 fun add_prf_rrule r = (Data.map o apfst) (cons (stamp (), r)); |
1348 fun add_prf_rproc p = (ProofData.map o apsnd) (cons (stamp (), p)); |
1348 fun add_prf_rproc p = (Data.map o apsnd) (cons (stamp (), p)); |
1349 |
1349 |
1350 |
1350 |
1351 (***** promises *****) |
1351 (***** promises *****) |
1352 |
1352 |
1353 fun promise_proof thy i prop = |
1353 fun promise_proof thy i prop = |