| changeset 63583 | a39baba12732 |
| parent 61932 | 2e48182cc82c |
| child 66453 | cc19f7ca2ed6 |
--- a/src/HOL/Isar_Examples/Knaster_Tarski.thy Tue Aug 02 18:13:24 2016 +0200 +++ b/src/HOL/Isar_Examples/Knaster_Tarski.thy Tue Aug 02 18:44:37 2016 +0200 @@ -7,7 +7,7 @@ section \<open>Textbook-style reasoning: the Knaster-Tarski Theorem\<close> theory Knaster_Tarski -imports Main "~~/src/HOL/Library/Lattice_Syntax" + imports Main "~~/src/HOL/Library/Lattice_Syntax" begin