| #
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;
|