Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Predicate_Compile.thy
author blanchet
Wed, 15 Dec 2010 11:26:28 +0100
changeset 41140 9c68004b8c9d
parent 40052 ea46574ca815
child 45450 dc2236b19a3d
permissions -rw-r--r--
added Sledgehammer support for higher-order propositional reasoning
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33265
01c9c6dbd890 proper headers;
wenzelm
parents: 33250
diff changeset 
     1
 
(*  Title:      HOL/Predicate_Compile.thy
01c9c6dbd890 proper headers;
wenzelm
parents: 33250
diff changeset 
     2
 
    Author:     Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen
01c9c6dbd890 proper headers;
wenzelm
parents: 33250
diff changeset 
     3
 
*)
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset 
     4
 












5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck



bulwahn


parents: 

diff
changeset




     5


header {* A compiler for predicates defined by introduction rules *}













5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck



bulwahn


parents: 

diff
changeset




     6














5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck



bulwahn


parents: 

diff
changeset




     7


theory Predicate_Compile








36021






c86fcf44b4c9
adopting Predicate_Compile



bulwahn


parents: 
35898

diff
changeset




     8


imports New_Random_Sequence








33250






5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck



bulwahn


parents: 

diff
changeset




     9


uses













5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck



bulwahn


parents: 

diff
changeset




    10


  "Tools/Predicate_Compile/predicate_compile_aux.ML"








36046






c3946372f556
putting compilation setup of predicate compiler in a separate file



bulwahn


parents: 
36032

diff
changeset




    11


  "Tools/Predicate_Compile/predicate_compile_compilations.ML"








40052






ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof



bulwahn


parents: 
36046

diff
changeset




    12


  "Tools/Predicate_Compile/core_data.ML"













ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof



bulwahn


parents: 
36046

diff
changeset




    13


  "Tools/Predicate_Compile/mode_inference.ML"













ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof



bulwahn


parents: 
36046

diff
changeset




    14


  "Tools/Predicate_Compile/predicate_compile_proof.ML"








33250






5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck



bulwahn


parents: 

diff
changeset




    15


  "Tools/Predicate_Compile/predicate_compile_core.ML"













5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck



bulwahn


parents: 

diff
changeset




    16


  "Tools/Predicate_Compile/predicate_compile_data.ML"













5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck



bulwahn


parents: 

diff
changeset




    17


  "Tools/Predicate_Compile/predicate_compile_fun.ML"













5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck



bulwahn


parents: 

diff
changeset




    18


  "Tools/Predicate_Compile/predicate_compile_pred.ML"








36032






dfd30b5b4e73
adding specialisation of predicates to the predicate compiler



bulwahn


parents: 
36021

diff
changeset




    19


  "Tools/Predicate_Compile/predicate_compile_specialisation.ML"








33250






5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck



bulwahn


parents: 

diff
changeset




    20


  "Tools/Predicate_Compile/predicate_compile.ML"













5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck



bulwahn


parents: 

diff
changeset




    21


begin













5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck



bulwahn


parents: 

diff
changeset




    22









33265






01c9c6dbd890
proper headers;



wenzelm


parents: 
33250

diff
changeset




    23


setup Predicate_Compile.setup








33250






5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck



bulwahn


parents: 

diff
changeset




    24









34948






2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck



bulwahn


parents: 
33265

diff
changeset




    25


end















isabelle