#
a270912e |
|
07-Nov-2014 |
wenzelm <none@none> |
proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
|
#
392cced7 |
|
18-Sep-2014 |
blanchet <none@none> |
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer) * * * made example compile again --HG-- rename : src/HOL/Old_Datatype.thy => src/HOL/Library/Old_Datatype.thy
|
#
fb2f6a3a |
|
01-Sep-2014 |
blanchet <none@none> |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place --HG-- rename : src/HOL/Datatype.thy => src/HOL/Old_Datatype.thy rename : src/HOL/Tools/Function/size.ML => src/HOL/Tools/Function/old_size.ML rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Old_Datatype/old_datatype.ML rename : src/HOL/Tools/Datatype/datatype_aux.ML => src/HOL/Tools/Old_Datatype/old_datatype_aux.ML rename : src/HOL/Tools/Datatype/datatype_codegen.ML => src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML rename : src/HOL/Tools/Datatype/datatype_data.ML => src/HOL/Tools/Old_Datatype/old_datatype_data.ML rename : src/HOL/Tools/Datatype/datatype_prop.ML => src/HOL/Tools/Old_Datatype/old_datatype_prop.ML rename : src/HOL/Tools/Datatype/datatype_realizer.ML => src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML rename : src/HOL/Tools/Datatype/primrec.ML => src/HOL/Tools/Old_Datatype/old_primrec.ML rename : src/HOL/Tools/Datatype/rep_datatype.ML => src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
|
#
aff4c530 |
|
24-May-2014 |
wenzelm <none@none> |
more portable file names; --HG-- rename : src/Doc/Tutorial/ToyList/ToyList1 => src/Doc/Tutorial/ToyList/ToyList1.txt rename : src/Doc/Tutorial/ToyList/ToyList2 => src/Doc/Tutorial/ToyList/ToyList2.txt
|