summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/ex/Guess.thy

author | bulwahn |

Fri Jan 07 14:46:28 2011 +0100 (2011-01-07) | |

changeset 41460 | ea56b98aee83 |

parent 20005 | 3fd6d57b16de |

child 58889 | 5b7a9633cfa8 |

permissions | -rw-r--r-- |

removing obselete Id comments from HOL/ex theories

1 (*

2 Author: Makarius

3 *)

5 header {* Proof by guessing *}

7 theory Guess

8 imports Main

9 begin

11 lemma True

12 proof

14 have 1: "\<exists>x. x = x" by simp

16 from 1 guess ..

17 from 1 guess x ..

18 from 1 guess x :: 'a ..

19 from 1 guess x :: nat ..

21 have 2: "\<exists>x y. x = x & y = y" by simp

22 from 2 guess apply - apply (erule exE conjE)+ done

23 from 2 guess x apply - apply (erule exE conjE)+ done

24 from 2 guess x y apply - apply (erule exE conjE)+ done

25 from 2 guess x :: 'a and y :: 'b apply - apply (erule exE conjE)+ done

26 from 2 guess x y :: nat apply - apply (erule exE conjE)+ done

28 qed

30 end