equal
deleted
inserted
replaced
451 |
451 |
452 |
452 |
453 (* header *) |
453 (* header *) |
454 |
454 |
455 fun mk_header (thy_name, parents) = |
455 fun mk_header (thy_name, parents) = |
456 (thy_name, "IsarThy.begin_theory " ^ cat (Library.quote thy_name) (mk_list parents) ^ " []"); |
456 (thy_name, "IsarThy.begin_theory " ^ cat (Library.quote thy_name) (mk_list parents) ^ " [] false"); |
457 |
457 |
458 val header = ident --$$ "=" -- enum1 "+" name >> mk_header; |
458 val header = ident --$$ "=" -- enum1 "+" name >> mk_header; |
459 |
459 |
460 |
460 |
461 (* extension *) |
461 (* extension *) |