src/HOL/Isar_examples/BasicLogic.thy
changeset 7005 cc778d613217
parent 7001 8121e11ed765
child 7133 64c9f2364dae
equal deleted inserted replaced
7004:c799d0859638 7005:cc778d613217
    25     show A; .;
    25     show A; .;
    26   qed;
    26   qed;
    27 qed;
    27 qed;
    28 
    28 
    29 lemma K': "A --> B --> A";
    29 lemma K': "A --> B --> A";
    30 proof single+; txt {* better use sufficient-to-show here \dots *};
    30 proof single+   -- {* better use sufficient-to-show here \dots *};
    31   assume A;
    31   assume A;
    32   show A; .;
    32   show A; .;
    33 qed;
    33 qed;
    34 
    34 
    35 lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
    35 lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";