CookBook/Package/Ind_Interface.thy
changeset 177 4e2341f6599d
parent 176 3da5f3f07d8b
child 178 fb8f22dd8ad0
equal deleted inserted replaced
176:3da5f3f07d8b 177:4e2341f6599d
   137       \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ 
   137       \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ 
   138       \"| oddS[intro]:  \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")
   138       \"| oddS[intro]:  \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")
   139 in
   139 in
   140   parse spec_parser input
   140   parse spec_parser input
   141 end"
   141 end"
   142 "((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []),
   142 "(((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]),
   143      [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
   143      [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
   144       ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
   144       ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
   145       ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
   145       ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
   146 *}
   146 *}
   147 
   147