2000-06-28 paulson 2000-06-28 new file Provers/make_elim.ML
2000-06-27 wenzelm 2000-06-27 replaced arities by instance;
2000-06-27 wenzelm 2000-06-27 OuterLex.name_of: include val;
2000-06-27 wenzelm 2000-06-27 excursion_result: transform_error;
2000-06-26 wenzelm 2000-06-26 eq_prop: eta contract;
2000-06-26 wenzelm 2000-06-26 tuned msg;
2000-06-26 wenzelm 2000-06-26 tuned;
2000-06-26 wenzelm 2000-06-26 avoid \< in input;
2000-06-26 wenzelm 2000-06-26 export proper induction rule;
2000-06-26 wenzelm 2000-06-26 bind_thm;
2000-06-26 oheimb 2000-06-26 corrected specifications and simplified proofs
2000-06-26 wenzelm 2000-06-26 isar-strip-terminators;
2000-06-26 wenzelm 2000-06-26 updated;
2000-06-26 wenzelm 2000-06-26 tuned;
2000-06-26 wenzelm 2000-06-26 use with_paths;
2000-06-25 wenzelm 2000-06-25 prefer mp over subst; tuned;
2000-06-25 wenzelm 2000-06-25 tuned;
2000-06-25 wenzelm 2000-06-25 Isar theory output.
2000-06-25 wenzelm 2000-06-25 Theory headers (old and new-style).
2000-06-25 wenzelm 2000-06-25 Text with antiquotations of inner items (terms, types etc.).
2000-06-25 wenzelm 2000-06-25 use Library.change;
2000-06-25 wenzelm 2000-06-25 adapted to improved presentation; no longer mirror items from structure Latex;
2000-06-25 wenzelm 2000-06-25 adapted to improved presentation;
2000-06-25 wenzelm 2000-06-25 excursion_result;
2000-06-25 wenzelm 2000-06-25 added extern_skolem;
2000-06-25 wenzelm 2000-06-25 moved header stuff to thy_header.ML; moved theory presentation to isar_output.ML; major cleanup;
2000-06-25 wenzelm 2000-06-25 added semicolon; added arguments; tuned;
2000-06-25 wenzelm 2000-06-25 added !!!; added is_semicolon; export incr_line, keep_line, scan_blank, scan_string; added source_proper; added make_lexicon; tuned;
2000-06-25 wenzelm 2000-06-25 use ThyHeader.args; adapted OuterSyntax.markup_command;
2000-06-25 wenzelm 2000-06-25 rearranged print commands;
2000-06-25 wenzelm 2000-06-25 exception OUTPUT_FAIL of (string * Position.T) * exn (*note: actually belongs to isar_output.ML*);
2000-06-25 wenzelm 2000-06-25 removed obsolete "{}";
2000-06-25 wenzelm 2000-06-25 added Isar/antiquote.ML, Isar/isar_output.ML, Isar/thy_header.ML;
2000-06-25 wenzelm 2000-06-25 added IsarOutput (token-level theory output);
2000-06-25 wenzelm 2000-06-25 added exhausted: ('a, 'b) source -> ('a, 'a list) source;
2000-06-25 wenzelm 2000-06-25 added state: 'a * 'b -> 'a * ('a * 'b);
2000-06-25 wenzelm 2000-06-25 fbrk: 2 if not taken;
2000-06-25 wenzelm 2000-06-25 export hidden: string -> string;
2000-06-25 wenzelm 2000-06-25 tuned;
2000-06-25 wenzelm 2000-06-25 added change: 'a ref -> ('a -> 'a) -> unit;
2000-06-23 berghofe 2000-06-23 Added new theory Lambda/Type.
2000-06-23 berghofe 2000-06-23 get_inductive now returns None instead of raising an exception.
2000-06-23 berghofe 2000-06-23 Added new theory.
2000-06-23 berghofe 2000-06-23 Subject reduction and strong normalization of simply-typed lambda terms.
2000-06-23 paulson 2000-06-23 new theorem trans_O_subset
2000-06-23 paulson 2000-06-23 added the AllocImpl example
2000-06-23 paulson 2000-06-23 genPrefix_trans_O: generalizes genPrefix_trans
2000-06-23 paulson 2000-06-23 added the allocator refinement proof
2000-06-23 paulson 2000-06-23 sum_below f n -> setsum f (lessThan n)
2000-06-22 wenzelm 2000-06-22 bind_thm(s);
2000-06-22 paulson 2000-06-22 removed some finiteness conditions from bag_of/sublist theorems
2000-06-22 paulson 2000-06-22 working proofs of the basic merge and distributor properties
2000-06-22 paulson 2000-06-22 fixed the merge spec (NbT -> Nclients) and added the distributor spec
2000-06-22 paulson 2000-06-22 new thoerem Always_Follows2; renamed Always_Follows -> Always_Follows1
2000-06-21 wenzelm 2000-06-21 added with_paths;
2000-06-21 wenzelm 2000-06-21 fixed deps;
2000-06-21 wenzelm 2000-06-21 fixed deps;
2000-06-21 wenzelm 2000-06-21 fixed deps;
2000-06-21 paulson 2000-06-21 new theorems lepoll_Ord_imp_eqpoll, lesspoll_imp_eqpoll, lesspoll_nat_is_Finite
2000-06-21 paulson 2000-06-21 new theorem UN_empty; it and Un_empty inserted by AddIffs