| author | eberlm <eberlm@in.tum.de> |
| Sat, 04 Aug 2018 01:03:39 +0200 | |
| changeset 68721 | 53ad5c01be3f |
| parent 67319 | 07176d5b81d5 |
| child 69605 | a96320074298 |
| permissions | -rw-r--r-- |
|
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 |
|
|
07176d5b81d5
moved 'realizers' into their own theory, now that they are decupled from the old datatype construction
blanchet
parents:
diff
changeset
|
11 |
ML_file "~~/src/HOL/Tools/datatype_realizer.ML" |
|
07176d5b81d5
moved 'realizers' into their own theory, now that they are decupled from the old datatype construction
blanchet
parents:
diff
changeset
|
12 |
ML_file "~~/src/HOL/Tools/inductive_realizer.ML" |
|
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 |