src/HOL/Tools/inductive_realizer.ML
2002-11-27 berghofe 2002-11-27 Changed format of realizers / correctness proofs.
2002-11-13 berghofe 2002-11-13 New package for constructing realizers for introduction and elimination rules of inductive predicates.