Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Realizers.thy
author wenzelm
Tue, 08 Oct 2024 12:10:35 +0200
changeset 81125 ec121999a9cb
parent 69605 a96320074298
permissions -rw-r--r--
more inner-syntax markup; more syntax bundles for use with "unbundle no foobar_syntax";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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















isabelle