src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
2010-03-29 bulwahn 2010-03-29 adding skip_proof in the examples because proof procedure cannot handle alternative compilations yet
2010-03-24 bulwahn 2010-03-24 adopting examples to Library move
2010-03-24 bulwahn 2010-03-24 moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session