isabelle: Graph

nodups -> distinct
2002-02-14, by nipkow
deleted some redundant 'addS*Es [equalityC*E]'s
2002-02-13, by paulson
new function lemmas
2002-02-13, by paulson
tidied. no more special simpset (super_ss)
2002-02-13, by paulson
new lemmas for closure under Union
2002-02-13, by paulson
eliminated Pure/Isar/comment.ML;
2002-02-12, by wenzelm
ANTIQUOTE_FAIL;
2002-02-12, by wenzelm
eliminated Isar/comment.ML;
2002-02-12, by wenzelm
tuned;
2002-02-12, by wenzelm
added isabelle-hol-book;
2002-02-12, by wenzelm
* Isar/Pure: marginal comments ``--'' may now occur just anywhere in the text;
2002-02-12, by wenzelm
got rid of explicit marginal comments (now stripped earlier from input);
2002-02-12, by wenzelm
tuned;
2002-02-12, by wenzelm
ML-Systems/smlnj-compiler.ML compatibility tweak;
2002-02-11, by wenzelm
include SVC_Test;
2002-02-11, by wenzelm
Theorems are only "pre-named" if the do not already have names.
2002-02-07, by berghofe
Added function could_unify to speed up rewriting of proof terms.
2002-02-06, by berghofe
Indexes of variables in expanded proofs are now incremented to avoid clashes.
2002-02-06, by berghofe
moved SVC stuff to ex;
2002-02-05, by wenzelm
New function maxidx_of_proof.
2002-02-05, by berghofe
New-style versions of these old examples
2002-02-04, by paulson
Rewrite procedure now works for both compact and full proof objects.
2002-02-02, by berghofe
escape_mfix;
2002-01-30, by wenzelm
added literal;
2002-01-30, by wenzelm
prep_mixfix': proper use of Syntax.literal;
2002-01-30, by wenzelm
tuned;
2002-01-30, by wenzelm
mu-syntax for the LEAST operator
2002-01-30, by paulson
Multiset: added the translation Mult(A) => A-||>nat-{0}
2002-01-30, by paulson
tuned;
2002-01-28, by wenzelm
GPLed;
2002-01-28, by wenzelm
tuned header;
2002-01-28, by wenzelm
tuned;
2002-01-28, by wenzelm
Bali added
2002-01-28, by schirmer
Isabelle/Bali sources;
2002-01-28, by schirmer
Isar cases/induct: no backtracking;
2002-01-26, by wenzelm
cases: really append cases_default;
2002-01-26, by wenzelm
generic DETERM;
2002-01-26, by wenzelm
ZF
2002-01-25, by paulson
copy_files *.sty;
2002-01-24, by wenzelm
cond_print_result_rule: priority (again) instead of slightly
2002-01-24, by wenzelm
fixed subgoal_tac; fails on non-existent subgoal;
2002-01-24, by wenzelm
copy_styles replaces overly conservative update_styles;
2002-01-24, by wenzelm
Springer LNCS 2283;
2002-01-24, by wenzelm
updated;
2002-01-24, by wenzelm
iff del: less_Suc0 -- luckily this does NOT affect the printed text;
2002-01-24, by wenzelm
delsimps [less_Suc0];
2002-01-23, by wenzelm
less_Suc0;
2002-01-23, by wenzelm
error "Unexpected end of input";
2002-01-23, by wenzelm
reorganized code for predicate text;
2002-01-23, by wenzelm
tuned;
2002-01-23, by wenzelm
* HOL: nat_number_of;
2002-01-23, by wenzelm
A few more standard simprules, TCs, etc.
2002-01-23, by paulson
qualified_result replaces qualified;
2002-01-22, by wenzelm
added locale_facts(_i) interface (useful for simple ML proof tools);
2002-01-22, by wenzelm
full_proofs;
2002-01-21, by wenzelm
* Pure/show_hyps reset by default (in accordance to existing Isar practice);
2002-01-21, by wenzelm
reset show_hyps by default (in accordance to existing Isar practice);
2002-01-21, by wenzelm
save library;
2002-01-21, by wenzelm
full_atomize;
2002-01-21, by wenzelm
wild guess at polyml-4.1.2;
2002-01-21, by wenzelm
options -l and -t;
2002-01-21, by wenzelm
Removed timing function.
2002-01-21, by berghofe
new simprules and classical rules
2002-01-21, by paulson
Tuned name mangling function.
2002-01-21, by berghofe
Made some proofs constructive.
2002-01-21, by berghofe
datatype_codegen now checks type of constructor.
2002-01-21, by berghofe
*** empty log message ***
2002-01-21, by nipkow
lexical tidying
2002-01-21, by paulson
slight re-use of code
2002-01-21, by paulson
fixed typos
2002-01-19, by kleing
rewrite_term: removed rew0, so no on-the-fly eta-contraction;
2002-01-18, by wenzelm
fixed document setup of HOL-Library;
2002-01-18, by wenzelm
tuned;
2002-01-18, by wenzelm
tidied
2002-01-18, by paulson
OOPS
2002-01-18, by paulson
tweaks
2002-01-18, by paulson
moved document sources to proper place, *within* Library/Library (!);
2002-01-18, by wenzelm
cover polyml-4.1.2;
2002-01-17, by wenzelm
RuleCases.make interface based on term instead of thm;
2002-01-17, by wenzelm
RuleCases.make interface based on term instead of thm;
2002-01-17, by wenzelm
atomize_term replaces atomize_cterm;
2002-01-17, by wenzelm
ObjectLogic.atomize_term replaces ObjectLogic.atomize_cterm;
2002-01-17, by wenzelm
Thm.prop_of;
2002-01-17, by wenzelm
Tactic.norm_hhf renamed to Tactic.norm_hhf_rule;
2002-01-17, by wenzelm
added prop_of: thm -> term (at last!);
2002-01-17, by wenzelm
added add_term_free_names (more precise/efficient than add_term_names);
2002-01-17, by wenzelm
renamed norm_hhf to norm_hhf_rule;
2002-01-17, by wenzelm
added is_norm_hhf (from logic.ML);
2002-01-17, by wenzelm
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
2002-01-17, by wenzelm
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
2002-01-17, by wenzelm
eta_contract with sharing (by berghofe);
2002-01-17, by wenzelm
is_norm_hhf moved to drule.ML;
2002-01-17, by wenzelm
added timeap_msg;
2002-01-17, by wenzelm
new style theory
2002-01-17, by nipkow
Lex dependencies modified
2002-01-17, by nipkow
Added code generation to Scanner.thy
2002-01-17, by nipkow
registered directly executable version with the code generator
2002-01-17, by kleing
*** empty log message ***
2002-01-17, by nipkow
new definitions from Sidi Ehmety
2002-01-17, by paulson
made proofs more robust
2002-01-17, by paulson
mistakenly deleted this theory
2002-01-17, by paulson
fixed
2002-01-17, by kleing
GPLed;
2002-01-16, by wenzelm
added rewrite_term;
2002-01-16, by wenzelm
interface to Pattern.rewrite_term;
2002-01-16, by wenzelm
tune norm_hhf_tac;
2002-01-16, by wenzelm
added beta_eta_contract;
2002-01-16, by wenzelm
tuned title;
2002-01-16, by wenzelm
export beta_eta_conversion;
2002-01-16, by wenzelm
Interface/proof_general.ML move to proof_general.ML;
2002-01-16, by wenzelm
Isar version of ZF/AC
2002-01-16, by paulson
Isar version of AC
2002-01-16, by paulson
norm_hhf;
2002-01-16, by wenzelm
fixed theory deps
2002-01-15, by kleing
use exec_lub instead of some_lub
2002-01-15, by kleing
tuned for directly executable definitions
2002-01-15, by kleing
tuned;
2002-01-15, by wenzelm
removed second copy of show_hyps;
2002-01-15, by wenzelm
tuned;
2002-01-15, by wenzelm
allow empty locales;
2002-01-15, by wenzelm
updated;
2002-01-15, by wenzelm
tuned;
2002-01-15, by wenzelm
new theorem
2002-01-15, by paulson
stylistic changes
2002-01-15, by paulson
now [rule_format] knows about ospec
2002-01-15, by paulson
split can now be unfolded even with one argument
2002-01-15, by paulson
save: be slightly more about absent tags;
2002-01-15, by wenzelm
allow zero goals;
2002-01-15, by wenzelm
tuned;
2002-01-15, by wenzelm
print_locale: allow full body specification;
2002-01-15, by wenzelm
added mk_conjunction_list;
2002-01-15, by wenzelm
conj_intr_list and conj_elim_precise: cover 0 conjuncts;
2002-01-15, by wenzelm
removed case_numbers (already covered by default);
2002-01-15, by wenzelm
Isar: undeclared rule case names default to numbers 1, 2, 3, ...;
2002-01-15, by wenzelm
* system: reduced base memory usage by Poly/ML (approx. 20 MB instead
2002-01-14, by wenzelm
ML_OPTIONS="-h 15000" (used to be 30000);
2002-01-14, by wenzelm
updated;
2002-01-14, by wenzelm
tuned;
2002-01-14, by wenzelm
updated;
2002-01-14, by wenzelm
tuned;
2002-01-14, by wenzelm
updated;
2002-01-14, by wenzelm
tuned;
2002-01-14, by wenzelm
updated;
2002-01-14, by wenzelm
tuned;
2002-01-14, by wenzelm
tuned;
2002-01-14, by wenzelm
cosmetics
2002-01-14, by oheimb
\<twosuperior> syntax moved to HOL/Numerals;
2002-01-13, by wenzelm
tuned;
2002-01-13, by wenzelm
prime_dvd_power_two;
2002-01-13, by wenzelm
symbolic syntax for x^2 (faills back on plain infix "^");
2002-01-13, by wenzelm
\usepackage[latin1]{inputenc};
2002-01-13, by wenzelm
* HOL: symbolic syntax for x^2 (numeral 2);
2002-01-13, by wenzelm
added HOL/Real/document/root.tex;
2002-01-13, by wenzelm
HOL-Real/Complex_Numbers;
2002-01-13, by wenzelm
Real/Complex_Numbers.thy;
2002-01-13, by wenzelm
tuned;
2002-01-12, by wenzelm
tuned;
2002-01-12, by wenzelm
produce predicate text;
2002-01-12, by wenzelm
added atomize_cterm;
2002-01-12, by wenzelm
tuned;
2002-01-12, by wenzelm
unify_frozen: proper use of maxidx';
2002-01-12, by wenzelm
paramify_dummies: proper treatment of maxidx;
2002-01-12, by wenzelm
renamed forall_elim_vars_safe to gen_all;
2002-01-12, by wenzelm
Isabelle2002 (January 2002);
2002-01-11, by wenzelm
removed obsolete isamode.ML;
2002-01-11, by wenzelm
tuned;
2002-01-11, by wenzelm
#!/usr/bin/env bash;
2002-01-11, by wenzelm
replace gen_all by forall_elim_vars_safe;
2002-01-11, by wenzelm
improved forall_elim_vars_safe (no longer invents new indexes);
2002-01-11, by wenzelm
lemmas (in ACe) AC;
2002-01-11, by wenzelm
tuned;
2002-01-11, by wenzelm
IsarThy.theorems_i;
2002-01-11, by wenzelm
moved setmksimps to Main!
2002-01-11, by wenzelm
have_thmss vs. have_thmss_i;
2002-01-11, by wenzelm
clarified/added theorems(_i) vs. locale_theorems(_i);
2002-01-11, by wenzelm
localized 'lemmas', 'theorems', 'declare';
2002-01-11, by wenzelm
have_thmss vs. have_thmss_i;
2002-01-11, by wenzelm
kind: ignore "";
2002-01-11, by wenzelm
IsarThy.theorems_i;
2002-01-11, by wenzelm
clarified IsarThy.apply_theorems_i;
2002-01-11, by wenzelm
* Pure: localized 'lemmas', 'theorems', 'declare';
2002-01-11, by wenzelm
removed add_thmss;
2002-01-10, by wenzelm
tuned;
2002-01-10, by wenzelm
export_single;
2002-01-10, by wenzelm
refine_tac: Tactic.norm_hhf_tac before trying rule;
2002-01-10, by wenzelm
add_thmss_hybrid;
2002-01-10, by wenzelm
export multi_theorem(_i), locale_multi_theorem(_i);
2002-01-10, by wenzelm
stylistic changes
2002-01-10, by paulson
*** empty log message ***
2002-01-10, by nipkow
locales: hide base name of exported version;
2002-01-10, by wenzelm
simplified theorem(_i);
2002-01-10, by wenzelm
IsarThy.smart_multi_theorem;
2002-01-10, by wenzelm
added hide_thms;
2002-01-10, by wenzelm
simplified IsarThy.theorem_i;
2002-01-10, by wenzelm
qualified exports from locales;
2002-01-10, by wenzelm
obsolete;
2002-01-09, by wenzelm
converted theory Transitive_Closure;
2002-01-09, by wenzelm
* added \<euro> symbol;
2002-01-09, by wenzelm
no longer requires TEXINPUTS;
2002-01-09, by wenzelm
isatool latex -o sty;
2002-01-09, by wenzelm
removed TEXINPUTS;
2002-01-09, by wenzelm
updated;
2002-01-09, by wenzelm
tuned;
2002-01-09, by wenzelm
updated;
2002-01-09, by wenzelm
tuned;
2002-01-09, by wenzelm
updated;
2002-01-09, by wenzelm
tuned;
2002-01-09, by wenzelm
tuned message;
2002-01-09, by wenzelm
changed the index sort key from |-| to just |- because pdflatex can't cope
2002-01-09, by paulson
HOL-Hyperreal produces an image (again);
2002-01-08, by wenzelm
dependencies for "typedef" image;
2002-01-08, by wenzelm
improved arrangement of "typedef" images;
2002-01-08, by wenzelm
no_document use_thy "While_Combinator";
2002-01-08, by wenzelm
tuned;
2002-01-08, by wenzelm
tuned;
2002-01-08, by wenzelm
tuned;
2002-01-08, by wenzelm
updated;
2002-01-08, by wenzelm
tuned;
2002-01-08, by wenzelm
\part{Elementary Techniques};
2002-01-08, by wenzelm
\chapter{The Basics};
2002-01-08, by wenzelm
Added some simprules proofs.
2002-01-08, by paulson
updated;
2002-01-08, by wenzelm
tuned;
2002-01-08, by wenzelm
added filter_filter
2002-01-08, by nipkow
#2 to 2
2002-01-08, by paulson
syntax "_not_equal";
2002-01-08, by wenzelm
removed (not really necessary, causes too many consistency problems);
2002-01-08, by wenzelm
tuned;
2002-01-08, by wenzelm
getting close to completion;
2002-01-07, by wenzelm
updated;
2002-01-07, by wenzelm
tuned;
2002-01-07, by wenzelm
updated;
2002-01-07, by wenzelm
tuned;
2002-01-07, by wenzelm
tuned deps;
2002-01-07, by wenzelm
tuned;
2002-01-07, by wenzelm
updated;
2002-01-07, by wenzelm
some more ...;
2002-01-06, by wenzelm
"_not_equal" dummy constant;
2002-01-06, by wenzelm
updated;
2002-01-06, by wenzelm
some more text;
2002-01-06, by wenzelm