1998-12-01 wenzelm 1998-12-01 excursion: ERROR_MESSAGE; exn_message: ERROR;
1998-12-01 wenzelm 1998-12-01 qed: kind_name (again);
1998-12-01 wenzelm 1998-12-01 show_tags flag;
1998-12-01 paulson 1998-12-01 new theorem INT_Un
1998-12-01 paulson 1998-12-01 better version of Image_diag
1998-11-30 paulson 1998-11-30 tactical CHANGED now uses alpha-eta conversion, not alpha conversion Streamlined code
1998-11-30 paulson 1998-11-30 Renamed subset_Sigma_llist to subset_Times_llist
1998-11-30 paulson 1998-11-30 new theorems about diag
1998-11-29 wenzelm 1998-11-29 fixed declatation of patterns and skolem;
1998-11-29 wenzelm 1998-11-29 tuned print_state; changed solve semantics: support back-pressure of asms (cut, def etc.);
1998-11-29 wenzelm 1998-11-29 tuned welcome msg;
1998-11-29 wenzelm 1998-11-29 added restart;
1998-11-29 wenzelm 1998-11-29 added exception RESTART;
1998-11-29 wenzelm 1998-11-29 proof_general_trans (experimental);
1998-11-29 wenzelm 1998-11-29 replaced wakeup by decorate_prompt_fn;
1998-11-29 wenzelm 1998-11-29 eliminated "Trying to recover ..." msg;
1998-11-29 wenzelm 1998-11-29 added oct_char;
1998-11-29 wenzelm 1998-11-29 method brute_force = ALLGOALS force_tac;
1998-11-27 nipkow 1998-11-27 *** empty log message ***
1998-11-27 nipkow 1998-11-27 At last: linear arithmetic for nat!
1998-11-27 nipkow 1998-11-27 Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
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;