| 2007-01-19 |
wenzelm |
renamed Isar/isar_output.ML to Thy/thy_output.ML;
|
file |
diff |
annotate
|
| 2007-01-05 |
haftmann |
added codegen_func.ML
|
file |
diff |
annotate
|
| 2007-01-05 |
wenzelm |
RAW-ProofGeneral: more dependencies;
|
file |
diff |
annotate
|
| 2007-01-04 |
wenzelm |
removed obsolete Pure-copied target;
|
file |
diff |
annotate
|
| 2006-12-30 |
wenzelm |
removed obsolete support for polyml-4.9.1;
|
file |
diff |
annotate
|
| 2006-12-29 |
wenzelm |
removed obsolete proof_general.ML;
|
file |
diff |
annotate
|
| 2006-12-10 |
wenzelm |
removed Isar/term_syntax.ML;
|
file |
diff |
annotate
|
| 2006-12-07 |
wenzelm |
added Isar/term_syntax.ML;
|
file |
diff |
annotate
|
| 2006-12-05 |
wenzelm |
added ML-Systems/polyml-5.0.ML;
|
file |
diff |
annotate
|
| 2006-12-05 |
aspinall |
Add dependency for new Emacs PG code
|
file |
diff |
annotate
|
| 2006-12-04 |
aspinall |
Build instructions for new Proof General module [not yet activated]
|
file |
diff |
annotate
|
| 2006-11-22 |
wenzelm |
added morphism.ML, General/ml_syntax.ML;
|
file |
diff |
annotate
|
| 2006-11-16 |
wenzelm |
moved some fundamental concepts to General/basics.ML;
|
file |
diff |
annotate
|
| 2006-11-13 |
wenzelm |
removed Isar/isar_thy.ML;
|
file |
diff |
annotate
|
| 2006-11-10 |
wenzelm |
removed obsolete ML compatibility fragments;
|
file |
diff |
annotate
|
| 2006-11-03 |
haftmann |
dropped name_mangler.ML
|
file |
diff |
annotate
|
| 2006-10-10 |
haftmann |
removed experimental codegen_simtype
|
file |
diff |
annotate
|
| 2006-10-09 |
wenzelm |
added General/secure.ML;
|
file |
diff |
annotate
|
| 2006-10-06 |
wenzelm |
added Isar/theory_target.ML;
|
file |
diff |
annotate
|
| 2006-09-27 |
wenzelm |
added ML-Systems/polyml-4.9.1.ML;
|
file |
diff |
annotate
|
| 2006-09-21 |
berghofe |
Added Tools/xml_syntax.ML
|
file |
diff |
annotate
|
| 2006-09-19 |
wenzelm |
added General/susp.ML;
|
file |
diff |
annotate
|
| 2006-09-19 |
haftmann |
code generation 2 adjustments
|
file |
diff |
annotate
|
| 2006-09-12 |
wenzelm |
added Pure/term_subst.ML;
|
file |
diff |
annotate
|
| 2006-08-14 |
haftmann |
added code generator packages
|
file |
diff |
annotate
|
| 2006-08-03 |
wenzelm |
added Isar/rule_insts.ML;
|
file |
diff |
annotate
|
| 2006-07-27 |
wenzelm |
added Pure/assumption.ML;
|
file |
diff |
annotate
|
| 2006-07-25 |
wenzelm |
added Pure/subgoal.ML;
|
file |
diff |
annotate
|
| 2006-07-11 |
wenzelm |
added name.ML;
|
file |
diff |
annotate
|
| 2006-06-15 |
wenzelm |
added variable.ML;
|
file |
diff |
annotate
|
| 2006-06-14 |
haftmann |
added codegen_simtype
|
file |
diff |
annotate
|
| 2006-06-10 |
dixon |
removed IsaPlanner - these are now in Provers.
|
file |
diff |
annotate
|
| 2006-06-07 |
wenzelm |
added Tools/invoke.ML;
|
file |
diff |
annotate
|
| 2006-04-13 |
wenzelm |
added conjunction.ML;
|
file |
diff |
annotate
|
| 2006-04-06 |
haftmann |
added definitional code generator module: codegen_theorems.ML
|
file |
diff |
annotate
|
| 2006-02-27 |
nipkow |
added nbe
|
file |
diff |
annotate
|
| 2006-02-21 |
nipkow |
added Tools/nbe
|
file |
diff |
annotate
|
| 2006-02-10 |
wenzelm |
added Isar/local_syntax.ML;
|
file |
diff |
annotate
|
| 2006-01-28 |
wenzelm |
added Isar/local_defs.ML;
|
file |
diff |
annotate
|
| 2006-01-23 |
webertj |
TimeLimit replaced by interrupt_timeout
|
file |
diff |
annotate
|
| 2006-01-22 |
wenzelm |
added Isar/local_theory.ML;
|
file |
diff |
annotate
|
| 2006-01-07 |
wenzelm |
added Isar/specification.ML;
|
file |
diff |
annotate
|
| 2005-12-12 |
haftmann |
added generic name mangler
|
file |
diff |
annotate
|
| 2005-11-14 |
haftmann |
added modules for code generator generation two, not operational yet
|
file |
diff |
annotate
|
| 2005-11-14 |
wenzelm |
added ML-Systems/polyml-4.1.4-patch.ML, ML-Systems/polyml-4.2.0.ML;
|
file |
diff |
annotate
|
| 2005-11-09 |
wenzelm |
added Isar/element.ML;
|
file |
diff |
annotate
|
| 2005-11-08 |
wenzelm |
renamed goals.ML to old_goals.ML;
|
file |
diff |
annotate
|
| 2005-11-02 |
wenzelm |
added consts.ML;
|
file |
diff |
annotate
|
| 2005-10-21 |
wenzelm |
added goal.ML;
|
file |
diff |
annotate
|
| 2005-10-19 |
wenzelm |
removed obsolete Thy/thy_parse.ML, Thy/thy_scan.ML, Thy/thy_syn.ML;
|
file |
diff |
annotate
|
| 2005-10-14 |
haftmann |
added module rat.ML for rational numbers
|
file |
diff |
annotate
|
| 2005-10-08 |
wenzelm |
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
|
file |
diff |
annotate
|
| 2005-09-13 |
wenzelm |
added General/stack.ML, Isar/proof_display.ML;
|
file |
diff |
annotate
|
| 2005-08-28 |
haftmann |
added alist.ML
|
file |
diff |
annotate
|
| 2005-08-16 |
wenzelm |
added Isar/outer_keyword.ML;
|
file |
diff |
annotate
|
| 2005-08-01 |
wenzelm |
added compress.ML;
|
file |
diff |
annotate
|
| 2005-07-12 |
obua |
- introduce Pure/Tools directory
|
file |
diff |
annotate
|
| 2005-06-22 |
wenzelm |
removed Pure/Isar/proof_data.ML, Pure/General/object.ML;
|
file |
diff |
annotate
|
| 2005-06-22 |
paulson |
pointer equality for sml/nj
|
file |
diff |
annotate
|
| 2005-06-18 |
wenzelm |
added Pure/General/ord_list.ML;
|
file |
diff |
annotate
|