equal
deleted
inserted
replaced
82 val gatherN = "gather"; |
82 val gatherN = "gather"; |
83 val atomsN = "atoms" |
83 val atomsN = "atoms" |
84 fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); |
84 fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); |
85 val any_keyword = keyword qeN || keyword gatherN || keyword atomsN; |
85 val any_keyword = keyword qeN || keyword gatherN || keyword atomsN; |
86 |
86 |
87 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; |
87 val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm); |
88 val terms = thms >> map Drule.dest_term; |
88 val terms = thms >> map Drule.dest_term; |
89 in |
89 in |
90 |
90 |
91 val _ = |
91 val _ = |
92 Theory.setup |
92 Theory.setup |