1998-11-27 paulson 1998-11-27 fixed a link
1998-11-27 paulson 1998-11-27 added Real/Hyperreal
1998-11-27 paulson 1998-11-27 Addition of Hyperreal theories Zorn and Filter
1998-11-27 paulson 1998-11-27 moved diag (diagonal relation) from Univ to Relation
1998-11-26 paulson 1998-11-26 tidied up list definitions, using type 'a option instead of unit + 'a, also using real typedefs instead of faking them with extra rules
1998-11-26 mueller 1998-11-26 tuning to assimiliate it with PhD;
1998-11-26 nipkow 1998-11-26 Added a general refutation tactic which works by putting things into nnf first.
1998-11-26 nipkow 1998-11-26 Added filter_prems_tac
1998-11-25 wenzelm 1998-11-25 removed prs / prs_fn;
1998-11-25 paulson 1998-11-25 guarantees laws
1998-11-25 paulson 1998-11-25 simplified ensures_UNIV
1998-11-25 paulson 1998-11-25 new thms for invariant
1998-11-25 paulson 1998-11-25 new theorem program_equalityE
1998-11-25 paulson 1998-11-25 renamed vars
1998-11-25 paulson 1998-11-25 image_id in simpset
1998-11-25 wenzelm 1998-11-25 removed prs / prs_fn (broken, because it did not include \n in its semantics, forcing writeln to add one uncoditionally); replaced prs_fn by writeln fn;
1998-11-25 wenzelm 1998-11-25 eliminated ISABELLE_INTERFACE_OPTIONS;
1998-11-25 wenzelm 1998-11-25 improved comment; removed ISABELLE_INTERFACE_OPTIONS; added ProofGeneral;
1998-11-25 wenzelm 1998-11-25 replaced prs by std_output;
1998-11-25 wenzelm 1998-11-25 replaced prs by writeln;
1998-11-25 wenzelm 1998-11-25 replaced prs by std_output / writeln;
1998-11-25 wenzelm 1998-11-25 comment parser;
1998-11-25 wenzelm 1998-11-25 add_text, add_chapter etc.: dummy;
1998-11-25 wenzelm 1998-11-25 chapter etc. headings; use, use_thy, cd: name;
1998-11-25 wenzelm 1998-11-25 tuned space;
1998-11-25 wenzelm 1998-11-25 replaced prs by writeln;
1998-11-25 wenzelm 1998-11-25 removed redirect_to_latex stuff;
1998-11-24 wenzelm 1998-11-24 Isar.main();
1998-11-24 wenzelm 1998-11-24 setup Blast.setup; setup Clasimp.setup;
1998-11-24 wenzelm 1998-11-24 added commands;
1998-11-24 wenzelm 1998-11-24 added isar.ML;
1998-11-24 wenzelm 1998-11-24 Isabelle/Isar main interface.
1998-11-24 wenzelm 1998-11-24 fixed prefix_lines: *separate* by \n;
1998-11-24 wenzelm 1998-11-24 added Isar/isar.ML;
1998-11-23 paulson 1998-11-23 fixed links
1998-11-21 wenzelm 1998-11-21 print_state hook, obeys Goals.current_goals_markers by default;
1998-11-21 wenzelm 1998-11-21 print_state: use begin_goal from Goals.current_goals_markers;
1998-11-21 wenzelm 1998-11-21 added undos, redos;
1998-11-21 wenzelm 1998-11-21 tty: issue wakeup;
1998-11-21 wenzelm 1998-11-21 std_output, prefix_lines;
1998-11-20 paulson 1998-11-20 better miniscoping rules: the premise C~={} is not good because Safe_tac eliminates such assumptions.
1998-11-19 wenzelm 1998-11-19 fixed method syntax;
1998-11-19 wenzelm 1998-11-19 break: exhibit state stack;
1998-11-19 wenzelm 1998-11-19 match_bind: 'as' patterns; statements: 'is' patterns;
1998-11-19 wenzelm 1998-11-19 let: 'as' patterns; statements: propp ('is' patterns);
1998-11-19 wenzelm 1998-11-19 match_bind(_i): 'as' patterns; assume, theorem, show etc.: propp; tuned qed msg;
1998-11-19 wenzelm 1998-11-19 term_pat vs. prop_pat; added bind_propp(_i); assume: propp;
1998-11-19 wenzelm 1998-11-19 term_pat vs. prop_pat;
1998-11-19 wenzelm 1998-11-19 no warning for "it" theorems;
1998-11-18 paulson 1998-11-18 tidied
1998-11-18 paulson 1998-11-18 Finally removing "Compl" from HOL
1998-11-18 wenzelm 1998-11-18 exn_message FAIL;
1998-11-18 wenzelm 1998-11-18 blast: cla_method';
1998-11-18 wenzelm 1998-11-18 export simp_modifiers;
1998-11-18 wenzelm 1998-11-18 expoer cla_method('), cla_modifiers;
1998-11-18 wenzelm 1998-11-18 method setup;
1998-11-18 wenzelm 1998-11-18 tuned comments;
1998-11-18 wenzelm 1998-11-18 'prop', 'term', 'typ';
1998-11-18 wenzelm 1998-11-18 load;
1998-11-18 wenzelm 1998-11-18 export exn_message;