CookBook/Package/Ind_Interface.thy
changeset 186 371e4375c994
parent 183 8bb4eaa2ec92
equal deleted inserted replaced
185:043ef82000b4 186:371e4375c994
   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 "(([(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