/src/HOL/Isar_Examples/
drwxr-xr-x [up]
drwxr-xr-x document
-rw-r--r-- 2015-12-07 16:44 +0000 14481 Basic_Logic.thy
-rw-r--r-- 2015-12-07 16:44 +0000 2537 Cantor.thy
-rw-r--r-- 2015-12-07 16:44 +0000 1449 Drinker.thy
-rw-r--r-- 2015-12-07 16:44 +0000 6936 Expr_Compiler.thy
-rw-r--r-- 2015-12-07 16:44 +0000 5341 Fibonacci.thy
-rw-r--r-- 2015-12-07 16:44 +0000 8845 Group.thy
-rw-r--r-- 2015-12-07 16:44 +0000 2828 Group_Context.thy
-rw-r--r-- 2015-12-07 16:44 +0000 2955 Group_Notepad.thy
-rw-r--r-- 2015-12-07 16:44 +0000 17052 Hoare.thy
-rw-r--r-- 2015-12-07 16:44 +0000 11676 Hoare_Ex.thy
-rw-r--r-- 2015-12-07 16:44 +0000 3911 Knaster_Tarski.thy
-rw-r--r-- 2015-12-07 16:44 +0000 9412 Mutilated_Checkerboard.thy
-rw-r--r-- 2015-12-07 16:44 +0000 1895 Nested_Datatype.thy
-rw-r--r-- 2015-12-07 16:44 +0000 3434 Peirce.thy
-rw-r--r-- 2015-12-07 16:44 +0000 2089 Puzzle.thy
-rw-r--r-- 2015-12-07 16:44 +0000 3101 Structured_Statements.thy
-rw-r--r-- 2015-12-07 16:44 +0000 5218 Summation.thy