equal
deleted
inserted
replaced
879 fun xmls_of_thy_goal (name,toks,str) = |
879 fun xmls_of_thy_goal (name,toks,str) = |
880 let |
880 let |
881 (* see isar_syn.ML/gen_theorem *) |
881 (* see isar_syn.ML/gen_theorem *) |
882 val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp); |
882 val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp); |
883 val general_statement = |
883 val general_statement = |
884 statement >> pair [] || Scan.repeat P.locale_elem_or_expr -- (P.$$$ "shows" |-- statement); |
884 statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement); |
885 |
885 |
886 val gen_theoremP = |
886 val gen_theoremP = |
887 P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --| |
887 P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --| |
888 Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) -- |
888 Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) -- |
889 general_statement >> (fn ((locale, a), (elems, concl)) => |
889 general_statement >> (fn ((locale, a), (elems, concl)) => |