#
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
cf26916d |
|
10-Nov-2018 |
wenzelm <none@none> |
added ML antiquotation @{master_dir};
|
#
5589896c |
|
12-Jan-2018 |
wenzelm <none@none> |
isabelle update_cartouches -c;
|
#
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;
|
#
6d4bb8c7 |
|
31-Oct-2014 |
wenzelm <none@none> |
provide explicit theory (amending 621c052789b4);
|
#
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
|
#
ee755a19 |
|
23-Jul-2014 |
wenzelm <none@none> |
more official Thy_Info.script_thy;
|
#
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
|
#
7216e79c |
|
18-Mar-2014 |
wenzelm <none@none> |
clarifed module name; --HG-- rename : src/Pure/Thy/thy_load.ML => src/Pure/PIDE/resources.ML rename : src/Pure/Thy/thy_load.scala => src/Pure/PIDE/resources.scala rename : src/Tools/jEdit/src/jedit_thy_load.scala => src/Tools/jEdit/src/jedit_resources.scala
|
#
62659e09 |
|
03-Sep-2013 |
wenzelm <none@none> |
more robust ToyList_Test;
|