isabelle: src/HOL/Library/Realizers.thy@a96320074298 (annotated)

67319 07176d5b81d5 moved 'realizers' into their own theory, now that they are decupled from the old datatype construction blanchet parents: diff changeset	1	(* Title: HOL/Library/Realizers.thy
07176d5b81d5 moved 'realizers' into their own theory, now that they are decupled from the old datatype construction blanchet parents: diff changeset	2	Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
07176d5b81d5 moved 'realizers' into their own theory, now that they are decupled from the old datatype construction blanchet parents: diff changeset	3	*)
07176d5b81d5 moved 'realizers' into their own theory, now that they are decupled from the old datatype construction blanchet parents: diff changeset	4
07176d5b81d5 moved 'realizers' into their own theory, now that they are decupled from the old datatype construction blanchet parents: diff changeset	5	section \<open>Program extraction from proofs involving datatypes and inductive predicates\<close>
07176d5b81d5 moved 'realizers' into their own theory, now that they are decupled from the old datatype construction blanchet parents: diff changeset	6
07176d5b81d5 moved 'realizers' into their own theory, now that they are decupled from the old datatype construction blanchet parents: diff changeset	7	theory Realizers
07176d5b81d5 moved 'realizers' into their own theory, now that they are decupled from the old datatype construction blanchet parents: diff changeset	8	imports Main
07176d5b81d5 moved 'realizers' into their own theory, now that they are decupled from the old datatype construction blanchet parents: diff changeset	9	begin
07176d5b81d5 moved 'realizers' into their own theory, now that they are decupled from the old datatype construction blanchet parents: diff changeset	10
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 67319 diff changeset	11	ML_file \<open>~~/src/HOL/Tools/datatype_realizer.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 67319 diff changeset	12	ML_file \<open>~~/src/HOL/Tools/inductive_realizer.ML\<close>
67319 07176d5b81d5 moved 'realizers' into their own theory, now that they are decupled from the old datatype construction blanchet parents: diff changeset	13
07176d5b81d5 moved 'realizers' into their own theory, now that they are decupled from the old datatype construction blanchet parents: diff changeset	14	end

author	wenzelm
	Sun, 06 Jan 2019 15:04:34 +0100
changeset 69605	a96320074298
parent 67319	07176d5b81d5
permissions	-rw-r--r--