author | nipkow |
Wed, 13 Feb 2019 07:48:42 +0100 | |
changeset 69801 | a99a0f5474c5 |
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