src/HOL/Tools/datatype_realizer.ML
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2002-11-27 berghofe 2002-11-27 Changed format of realizers / correctness proofs.
2002-11-13 berghofe 2002-11-13 prove_goal' -> Goal.simple_prove_goal_cterm
2002-10-21 berghofe 2002-10-21 Changed type of Logic.strip_horn.
2002-10-10 berghofe 2002-10-10 Reimplemented parts of datatype package dealing with datatypes involving function types. Now also supports functions with more than one argument.
2002-08-07 berghofe 2002-08-07 Module for defining realizers for induction and case analysis theorems for datatypes.