112 [Const (\"all\", \<dots>) $ Abs (\"x\", TFree (\"'a\", \<dots>), |
112 [Const (\"all\", \<dots>) $ Abs (\"x\", TFree (\"'a\", \<dots>), |
113 Const (\"all\", \<dots>) $ Abs (\"y\", TFree (\"'a\", \<dots>), |
113 Const (\"all\", \<dots>) $ Abs (\"y\", TFree (\"'a\", \<dots>), |
114 Const (\"all\", \<dots>) $ Abs (\"z\", TFree (\"'a\", \<dots>), |
114 Const (\"all\", \<dots>) $ Abs (\"z\", TFree (\"'a\", \<dots>), |
115 Const (\"==>\", \<dots>) $ |
115 Const (\"==>\", \<dots>) $ |
116 (Const (\"Trueprop\", \<dots>) $ |
116 (Const (\"Trueprop\", \<dots>) $ |
117 (Free (\"trcl\", \<dots>) $ Free (\"r\", \<dots>) $ Bound 2 $ Bound 1)) $ |
117 (Free (\"trcl\", \<dots>) $ Free (\"r\", \<dots>) $ Bound 2 $ Bound 1)) $ |
118 (Const (\"==>\", \<dots>) $ \<dots> $ \<dots>))))])]), |
118 (Const (\"==>\", \<dots>) $ \<dots> $ \<dots>))))])]), |
119 \<dots>) |
119 \<dots>) |
120 : (((Name.binding * typ) * mixfix) list * |
120 : (((Name.binding * typ) * mixfix) list * |
121 (Attrib.binding * term list) list) * local_theory"} |
121 (Attrib.binding * term list) list) * local_theory"} |
122 In the list of variables passed to @{ML_open read_specification (Specification)}, we have |
122 In the list of variables passed to @{ML_open read_specification (Specification)}, we have |