author | wenzelm |
Mon, 11 Sep 2023 19:30:48 +0200 | |
changeset 78659 | b5f3d1051b13 |
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