275 |
275 |
276 For parsing and type checking the introduction rules, we use the function |
276 For parsing and type checking the introduction rules, we use the function |
277 |
277 |
278 @{ML [display] "Specification.read_specification: |
278 @{ML [display] "Specification.read_specification: |
279 (Binding.binding * string option * mixfix) list -> (*{variables}*) |
279 (Binding.binding * string option * mixfix) list -> (*{variables}*) |
280 (Attrib.binding * string list) list list -> (*{rules}*) |
280 (Attrib.binding * string list) list -> (*{rules}*) |
281 local_theory -> |
281 local_theory -> |
282 (((Binding.binding * typ) * mixfix) list * |
282 (((Binding.binding * typ) * mixfix) list * |
283 (Attrib.binding * term list) list) * |
283 (Attrib.binding * term list) list) * |
284 local_theory"} |
284 local_theory"} |
285 *} |
285 *} |
313 |
313 |
314 @{ML_response [display] |
314 @{ML_response [display] |
315 "Specification.read_specification |
315 "Specification.read_specification |
316 [(Binding.name \"trcl\", NONE, NoSyn), |
316 [(Binding.name \"trcl\", NONE, NoSyn), |
317 (Binding.name \"r\", SOME \"'a \<Rightarrow> 'a \<Rightarrow> bool\", NoSyn)] |
317 (Binding.name \"r\", SOME \"'a \<Rightarrow> 'a \<Rightarrow> bool\", NoSyn)] |
318 [[((Binding.name \"base\", []), [\"trcl r x x\"])], |
318 [((Binding.name \"base\", []), [\"trcl r x x\"]), |
319 [((Binding.name \"step\", []), [\"trcl r x y \<Longrightarrow> r y z \<Longrightarrow> trcl r x z\"])]] |
319 ((Binding.name \"step\", []), [\"trcl r x y \<Longrightarrow> r y z \<Longrightarrow> trcl r x z\"])] |
320 @{context}" |
320 @{context}" |
321 "((\<dots>, |
321 "((\<dots>, |
322 [(\<dots>, |
322 [(\<dots>, |
323 [Const (\"all\", \<dots>) $ Abs (\"x\", TFree (\"'a\", \<dots>), |
323 [Const (\"all\", \<dots>) $ Abs (\"x\", TFree (\"'a\", \<dots>), |
324 Const (\"Trueprop\", \<dots>) $ |
324 Const (\"Trueprop\", \<dots>) $ |