CookBook/Package/Ind_Interface.thy
changeset 176 3da5f3f07d8b
parent 129 e0d368a45537
child 177 4e2341f6599d
equal deleted inserted replaced
175:7c09bd3227c5 176:3da5f3f07d8b
   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>) $