449 raise error ("assoc_thm': '"^thmid^"' not in '"^ |
449 raise error ("assoc_thm': '"^thmid^"' not in '"^ |
450 (theory2domID thy)^"' (and parents)"); |
450 (theory2domID thy)^"' (and parents)"); |
451 (*> assoc_thm' Isac.thy ("sym_#mult_2_3","6 = 2 * 3"); |
451 (*> assoc_thm' Isac.thy ("sym_#mult_2_3","6 = 2 * 3"); |
452 val it = "6 = 2 * 3" : thm |
452 val it = "6 = 2 * 3" : thm |
453 |
453 |
454 > assoc_thm' Isac.thy ("real_add_zero_left",""); |
454 > assoc_thm' Isac.thy ("add_0_left",""); |
455 val it = "0 + ?z = ?z" : thm |
455 val it = "0 + ?z = ?z" : thm |
456 |
456 |
457 > assoc_thm' Isac.thy ("sym_real_add_zero_left",""); |
457 > assoc_thm' Isac.thy ("sym_real_add_zero_left",""); |
458 val it = "?t = 0 + ?t" [.] : thm |
458 val it = "?t = 0 + ?t" [.] : thm |
459 |
459 |
460 > assoc_thm' HOL.thy ("sym_real_add_zero_left",""); |
460 > assoc_thm' HOL.thy ("sym_real_add_zero_left",""); |
461 *** Unknown theorem(s) "real_add_zero_left" |
461 *** Unknown theorem(s) "add_0_left" |
462 *** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents) |
462 *** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents) |
463 uncaught exception ERROR*) |
463 uncaught exception ERROR*) |
464 |
464 |
465 |
465 |
466 fun parse' (thy:theory') (ct:cterm') = |
466 fun parse' (thy:theory') (ct:cterm') = |