summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/ex/cla.ML

changeset 2997 | 86aaab39ebb1 |

parent 2922 | 580647a879cf |

child 3019 | ca5a7bbbee6c |

equal
deleted
inserted
replaced

2996:2a311f90747c | 2997:86aaab39ebb1 |
---|---|

16 by (Blast_tac 1); |
16 by (Blast_tac 1); |

17 result(); |
17 result(); |

18 |
18 |

19 (*If and only if*) |
19 (*If and only if*) |

20 |
20 |

21 goal HOL.thy "(P=Q) = (Q=P::bool)"; |
21 goal HOL.thy "(P=Q) = (Q = (P::bool))"; |

22 by (Blast_tac 1); |
22 by (Blast_tac 1); |

23 result(); |
23 result(); |

24 |
24 |

25 goal HOL.thy "~ (P = (~P))"; |
25 goal HOL.thy "~ (P = (~P))"; |

26 by (Blast_tac 1); |
26 by (Blast_tac 1); |