changeset 66453 | cc19f7ca2ed6 |
parent 60117 | 2712f40d6309 |
child 69597 | ff784d5a5bfb |
66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
---|---|
1 theory Rewrite_Examples |
1 theory Rewrite_Examples |
2 imports Main "~~/src/HOL/Library/Rewrite" |
2 imports Main "HOL-Library.Rewrite" |
3 begin |
3 begin |
4 |
4 |
5 section \<open>The rewrite Proof Method by Example\<close> |
5 section \<open>The rewrite Proof Method by Example\<close> |
6 |
6 |
7 (* This file is intended to give an overview over |
7 (* This file is intended to give an overview over |