thys/Exercises.thy
changeset 266 fff2e1b40dfc
parent 260 160d0b08471c
child 268 6746f5e1f1f8
equal deleted inserted replaced
265:d36be1e356c0 266:fff2e1b40dfc
     1 theory Exercises
     1 theory Exercises
     2   imports Lexer "~~/src/HOL/Library/Infinite_Set"
     2   imports Spec "~~/src/HOL/Library/Infinite_Set"
     3 begin
     3 begin
     4 
     4 
     5 section {* Some Fun Facts *}
     5 section {* Some Fun Facts *}
     6 
     6 
     7 fun
     7 fun