# HG changeset patch # User wenzelm # Date 1244717420 -7200 # Node ID 318081898306009dc57eb8387ad22d8ec0dec8cd # Parent a6c6bf2751a096e17fb3869c326b5a937a118cae theory Predicate_Compile_ex: enable quick_and_dirty for now, to make it work with internal cheat_tac invocations; diff -r a6c6bf2751a0 -r 318081898306 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Thu Jun 11 12:48:38 2009 +0200 +++ b/src/HOL/ex/ROOT.ML Thu Jun 11 12:50:20 2009 +0200 @@ -14,10 +14,11 @@ "Codegenerator_Pretty_Test", "NormalForm", "../NumberTheory/Factorization", - "Predicate_Compile", - "Predicate_Compile_ex" + "Predicate_Compile" ]; +setmp quick_and_dirty true use_thy "Predicate_Compile_ex"; + use_thys [ "Numeral", "Higher_Order_Logic",