Added some files for doing demos, and added a filter to avoid proving theorems that are in Isabelle's library but not available to simp, by using Find_Theorems.