isabelle: src/HOL/Library/Realizers.thy@972c0c744e7c (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	haftmann
	Fri, 14 Jun 2019 08:34:27 +0000
changeset 70341	972c0c744e7c
parent 69605	a96320074298
permissions	-rw-r--r--