2007-07-08 wenzelm 2007-07-08 renamed ML_exc to ML_exn;
2007-07-08 chaieb 2007-07-08 Show the use of reflection attribute; fixed comments about the order of absorbing equations : f (C x) = x ; now automaically tried as last;
2007-07-08 chaieb 2007-07-08 Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
2007-07-08 chaieb 2007-07-08 Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
2007-07-08 chaieb 2007-07-08 Context data now consist of eqations for reification and equations for correctness theorems for reflection; Added attribute reflection to store correctness theorems to be trued by default
2007-07-08 wenzelm 2007-07-08 simplified/more robust print_state; more robust prompt markup;
2007-07-08 wenzelm 2007-07-08 export mode_markup; added symbolic output (via print_mode); misc cleanup;
2007-07-08 wenzelm 2007-07-08 added markup for pretty printing;
2007-07-08 chaieb 2007-07-08 Corrected erronus use of compiletime context to the runtime context
2007-07-07 wenzelm 2007-07-07 make smlnj happy;
2007-07-07 wenzelm 2007-07-07 toplevel prompt/print_state: proper markup, removed hooks;
2007-07-07 wenzelm 2007-07-07 toplevel prompt/print_state: proper markup, removed hooks; tuned;
2007-07-07 wenzelm 2007-07-07 pretty_state: subgoal markup; tuned;
2007-07-07 wenzelm 2007-07-07 added markup_chunks;
2007-07-07 wenzelm 2007-07-07 added toplevel markup; misc cleanup;
2007-07-07 wenzelm 2007-07-07 use markup.ML earlier;
2007-07-07 wenzelm 2007-07-07 removed obsolete disable_pr/enable_pr; added old print_goals from display.ML;
2007-07-07 wenzelm 2007-07-07 pretty_goals_aux: subgoal markup; print_goals etc.: moved old version to old_goals.ML, removed hooks; tuned;
2007-07-07 wenzelm 2007-07-07 pr_goals: adapted Display.pretty_goals_aux; pr_goals/prterm: proper context; tuned;
2007-07-07 wenzelm 2007-07-07 export attribute;
2007-07-07 wenzelm 2007-07-07 pretty_sort/typ/term: markup;
2007-07-07 wenzelm 2007-07-07 pretty: markup for syntax/name of authentic consts; datatype symb: String (potential markup) vs. Space (no markup);
2007-07-07 wenzelm 2007-07-07 depend on alist.ML, markup.ML;
2007-07-07 wenzelm 2007-07-07 markup: emit as control information -- no indent text;
2007-07-07 wenzelm 2007-07-07 added property conversions; tuned;
2007-07-07 wenzelm 2007-07-07 position: line and name; tuned operations;
2007-07-07 wenzelm 2007-07-07 moved markup.ML before position.ML;
2007-07-07 chaieb 2007-07-07 The order for parameter for interpretation is now inversted: f t env0 env1 ... envn = ... where t is the type to be reified;
2007-07-07 wenzelm 2007-07-07 Common markup elements.
2007-07-07 wenzelm 2007-07-07 simplified pretty token metric: type int; added command markup; token translations: proper treatment of skolems; separate print_mode setup for Output/Pretty;
2007-07-07 wenzelm 2007-07-07 simplified pretty token metric: type int; separate print_mode setup for Output/Pretty;
2007-07-07 wenzelm 2007-07-07 moved General/xml.ML to Tools/xml.ML; actually use pgml.ML;
2007-07-07 wenzelm 2007-07-07 tuned;
2007-07-07 wenzelm 2007-07-07 simplified output mode setup; removed unused symbol_output; tuned;
2007-07-07 wenzelm 2007-07-07 added print_mode setup: indent and markup; simplified pretty token metric: type int; added general markup for blocks; removed unused writelns;
2007-07-07 wenzelm 2007-07-07 renamed raw to escape; simplified pretty token metric: type int; simplified print_mode setup: output_width and escape; moved pretty setup to pretty.ML;
2007-07-07 wenzelm 2007-07-07 simplified pretty token metric: type int;
2007-07-07 wenzelm 2007-07-07 moved General/xml.ML to Tools/xml.ML;
2007-07-07 wenzelm 2007-07-07 added General/markup.ML; moved General/xml.ML to Tools/xml.ML;
2007-07-07 wenzelm 2007-07-07 added class skolem, command;
2007-07-06 nipkow 2007-07-06 more interpretations
2007-07-06 aspinall 2007-07-06 Produce good PGML 2.0
2007-07-06 webertj 2007-07-06 cosmetic (line length fixed)
2007-07-06 chaieb 2007-07-06 Some examples for reifying type variables
2007-07-06 chaieb 2007-07-06 Tuned document
2007-07-06 chaieb 2007-07-06 Cleaned add and del attributes
2007-07-06 chaieb 2007-07-06 Reification now deals with type variables
2007-07-06 wenzelm 2007-07-06 Cumulative reports for Poly/ML profiling output.
2007-07-05 aspinall 2007-07-05 Update PGML version, add system name
2007-07-05 wenzelm 2007-07-05 tuned interfaces: atomize, atomize_prems, atomize_prems_tac; removed atomize_cterm/goal;
2007-07-05 wenzelm 2007-07-05 added type conv; merge_thys: removed dead exception handlers; tuned;
2007-07-05 wenzelm 2007-07-05 removed comments -- no exception TERM; merge_list: exception THEORY;
2007-07-05 wenzelm 2007-07-05 added is_reflexive;
2007-07-05 wenzelm 2007-07-05 tuned;
2007-07-05 wenzelm 2007-07-05 simplified has_meta_prems;
2007-07-05 wenzelm 2007-07-05 moved type conv to thm.ML; renamed Conv.is_refl to Thm.is_reflexive; misc tuning of basic conversions;
2007-07-05 wenzelm 2007-07-05 the_theory/proof: error instead of exception Fail;
2007-07-05 wenzelm 2007-07-05 renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac; added flat_rule filter for addXXs etc.;
2007-07-05 wenzelm 2007-07-05 renamed Conv.is_refl to Thm.is_reflexive;
2007-07-05 wenzelm 2007-07-05 renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac; simplified ObjectLogic.atomize;