isabelle: src/HOL/Predicate_Compile.thy@61dd8c145da7

     1 (*  Title:      HOL/Predicate_Compile.thy

     2     Author:     Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen

     3 *)

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

     7 theory Predicate_Compile

     8 imports New_Random_Sequence

     9 uses

    10   "Tools/Predicate_Compile/predicate_compile_aux.ML"

    11   "Tools/Predicate_Compile/predicate_compile_compilations.ML"

    12   "Tools/Predicate_Compile/predicate_compile_core.ML"

    13   "Tools/Predicate_Compile/predicate_compile_data.ML"

    14   "Tools/Predicate_Compile/predicate_compile_fun.ML"

    15   "Tools/Predicate_Compile/predicate_compile_pred.ML"

    16   "Tools/Predicate_Compile/predicate_compile_specialisation.ML"

    17   "Tools/Predicate_Compile/predicate_compile.ML"

    18 begin

    20 setup Predicate_Compile.setup

    22 end

author	haftmann
	Fri Jun 11 17:14:02 2010 +0200 (2010-06-11)
changeset 37407	61dd8c145da7
parent 36046	c3946372f556
child 40052	ea46574ca815
permissions	-rw-r--r--