2007-07-09 wenzelm 2007-07-09 use position.ML after pretty.ML;
2007-07-09 wenzelm 2007-07-09 removed target RAW-ProofGeneral (impractical to maintain);
2007-07-09 wenzelm 2007-07-09 declare: disallow quote (") in names;
2007-07-09 wenzelm 2007-07-09 removed legacy ML file; fixed prems_conv;
2007-07-09 wenzelm 2007-07-09 HOL-Complex-Matrix: fixed deps -- sort of;
2007-07-09 obua 2007-07-09 adopted to new computing oracle and fixed bugs introduced by tuning
2007-07-09 obua 2007-07-09 added computing oracle support for HOL and numerals
2007-07-09 obua 2007-07-09 new version of computing oracle
2007-07-09 wenzelm 2007-07-09 simplified writeln_fn;
2007-07-09 wenzelm 2007-07-09 prompt: plain string, not output;
2007-07-09 wenzelm 2007-07-09 type output = string indicates raw system output;
2007-07-08 wenzelm 2007-07-08 symbolic output: avoid empty blocks, 1 space for fbreak;
2007-07-08 wenzelm 2007-07-08 tuned;
2007-07-08 wenzelm 2007-07-08 thm tag: Markup.property list;
2007-07-08 wenzelm 2007-07-08 gensym: slightly more obscure prefix descreases probability of name clash;
2007-07-08 wenzelm 2007-07-08 replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-07-08 wenzelm 2007-07-08 attribute tagged: single argument;
2007-07-08 wenzelm 2007-07-08 updated;
2007-07-08 wenzelm 2007-07-08 simplified Symtab;
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