author | nipkow |
Thu, 13 Sep 2018 06:36:00 +0200 | |
changeset 68983 | caedabd2771c |
parent 67319 | 07176d5b81d5 |
child 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 "~~/src/HOL/Tools/datatype_realizer.ML" ML_file "~~/src/HOL/Tools/inductive_realizer.ML" end