*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Isar syntax question*From*: Vadim Zaliva <vzaliva at cmu.edu>*Date*: Wed, 16 Jul 2014 15:00:19 -0700*Sender*: Vadim Zaliva <vadim.zaliva at west.cmu.edu>

I am learning Isar and have another naive question on the syntax: I am trying to do something like this in Isar: 1: lemma 2: shows "not something" 3: proof(rule ccontr) 4: assume "something" 5: thus False proof cases 6: ... 7: qed 8: qed and get "*** Failed to refine any pending goal" error around line 5 Why this does not work? Something like this works instead: lemma shows "not something" proof assume "something" hence False proof cases ... qed thus False by simp qed But last statement (thus False by simp) seems to be unnecessary, as it is proving False from False! Sincerely, Vadim Zaliva -- CMU ECE PhD student Mobile: +1(510)220-1060 Skype: vzaliva

**Follow-Ups**:**Re: [isabelle] Isar syntax question***From:*Timothy Bourke

**Re: [isabelle] Isar syntax question***From:*Lars Noschinski

**Re: [isabelle] Isar syntax question***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP
- Next by Date: Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP
- Previous by Thread: Re: [isabelle] Isabelle2014-RC0: vertical spacing bad pg.9 of locales.pdf
- Next by Thread: Re: [isabelle] Isar syntax question
- Cl-isabelle-users July 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list