1998-08-27 wenzelm 1998-08-27 made tutorial first;
1998-08-27 wenzelm 1998-08-27 tuned;
1998-08-27 wenzelm 1998-08-27 exec;
1998-08-27 wenzelm 1998-08-27 * Pure: ML function 'theory_of' replaced by 'theory';
1998-08-27 wenzelm 1998-08-27 tuned;
1998-08-27 wenzelm 1998-08-27 isatool install;
1998-08-27 wenzelm 1998-08-27 added tutorial;
1998-08-27 wenzelm 1998-08-27 fixed ISABELLE_USEDIR_OPTIONS;
1998-08-27 wenzelm 1998-08-27 *** empty log message ***
1998-08-27 wenzelm 1998-08-27 Goal, Goalw; thm, thms; moved get_thm etc. from theories.tex;
1998-08-27 wenzelm 1998-08-27 moeved get_thm etc. to goals.tex;
1998-08-27 wenzelm 1998-08-27 tuned doc name;
1998-08-27 wenzelm 1998-08-27 fixed center;
1998-08-27 wenzelm 1998-08-27 ISABELLE_USEDIR_OPTIONS="-i false";
1998-08-27 wenzelm 1998-08-27 tuned; added ISABELLE_USEDIR_OPTIONS;
1998-08-27 wenzelm 1998-08-27 eps logis;
1998-08-27 wenzelm 1998-08-27 href eps versions;
1998-08-27 wenzelm 1998-08-27 weblinted, tuned;
1998-08-27 wenzelm 1998-08-27 fake proper eps header;
1998-08-26 wenzelm 1998-08-26 fixed tutorial;
1998-08-26 wenzelm 1998-08-26 added HOL tutorial;
1998-08-26 wenzelm 1998-08-26 added HOL tutorial;
1998-08-26 nipkow 1998-08-26 junk
1998-08-26 nipkow 1998-08-26 *** empty log message ***
1998-08-26 nipkow 1998-08-26 *** empty log message ***
1998-08-26 nipkow 1998-08-26 The HOL tutorial.
1998-08-26 wenzelm 1998-08-26 moved images to gfx dir;
1998-08-24 wenzelm 1998-08-24 tuned;
1998-08-24 wenzelm 1998-08-24 SYNC;
1998-08-24 wenzelm 1998-08-24 emacs local vars;
1998-08-24 wenzelm 1998-08-24 emacs local vars; added conversions (Simplifier.rewrite etc.); updated tracing example; fixed theory setup;
1998-08-24 wenzelm 1998-08-24 added nonterminals, setup; removed print_data;
1998-08-24 wenzelm 1998-08-24 added Antiquote example;
1998-08-24 wenzelm 1998-08-24 mkdir -p;
1998-08-24 wenzelm 1998-08-24 emacs local vars; isatool install;
1998-08-24 wenzelm 1998-08-24 SYNC;
1998-08-24 wenzelm 1998-08-24 emacs local vars;
1998-08-24 wenzelm 1998-08-24 isatool install;
1998-08-24 wenzelm 1998-08-24 install binaries with absolute references to ISABELLE_HOME/bin;
1998-08-24 oheimb 1998-08-24 debugged split_eta_proc
1998-08-21 paulson 1998-08-21 tidied
1998-08-21 paulson 1998-08-21 Tidying
1998-08-21 paulson 1998-08-21 New UNITY files
1998-08-20 paulson 1998-08-20 New theory Lift
1998-08-20 paulson 1998-08-20 new theorems
1998-08-20 paulson 1998-08-20 tidied
1998-08-20 paulson 1998-08-20 new theorems; adds [le_refl, less_imp_le] as simprules
1998-08-20 paulson 1998-08-20 adjusted for new rewrites
1998-08-20 paulson 1998-08-20 tidied
1998-08-20 paulson 1998-08-20 tidied
1998-08-20 paulson 1998-08-20 Must remove leD from simpset
1998-08-20 paulson 1998-08-20 tidied
1998-08-20 paulson 1998-08-20 Must remove less_imp_le from simpset
1998-08-20 nipkow 1998-08-20 Added converse_rtranclE(2)
1998-08-20 paulson 1998-08-20 Now qed_spec_mp respects locales, by calling ml_store_thm instead of bind_thm
1998-08-19 wenzelm 1998-08-19 fixed param;
1998-08-19 wenzelm 1998-08-19 assume: adjust_maxidx;
1998-08-19 paulson 1998-08-19 new version, more resistant to PROOF FAILED. Now it distinguishes between inferences that update the branch (resolve_tac) and those that do not (match_tac)
1998-08-19 paulson 1998-08-19 The warning "Rewrite rule from different theory" is ALWAYS printed, even if tracing is off.
1998-08-19 paulson 1998-08-19 new theorem zero_less_diff