src/HOL/Predicate_Compile_Examples/ROOT.ML
author bulwahn
Tue, 07 Sep 2010 11:51:53 +0200
changeset 39184 71f3f194b962
parent 38948 c4e6afaa8dcd
child 39185 c035d01a7e77
permissions -rw-r--r--
adding a List example (challenge from Tobias) for counterexample search

use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"];
if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Hotel_Example", "Lambda_Example", "List_Examples"];