author | haftmann |
Mon, 14 Jan 2019 18:35:03 +0000 | |
changeset 69661 | a03a63b81f44 |
parent 69605 | a96320074298 |
permissions | -rw-r--r-- |
(* Title: HOL/Library/Realizers.thy Author: Stefan Berghofer and Markus Wenzel, TU Muenchen *) section \<open>Program extraction from proofs involving datatypes and inductive predicates\<close> theory Realizers imports Main begin ML_file \<open>~~/src/HOL/Tools/datatype_realizer.ML\<close> ML_file \<open>~~/src/HOL/Tools/inductive_realizer.ML\<close> end