isabelle: Graph

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
updated;
2002-01-06, by wenzelm
tuned;
2002-01-06, by wenzelm
some text on document preparation;
2002-01-05, by wenzelm
updated;
2002-01-05, by wenzelm
tuned;
2002-01-05, by wenzelm
updated;
2002-01-05, by wenzelm
mention X-Symbol;
2002-01-05, by wenzelm
updated;
2002-01-05, by wenzelm
use wasysym package;
2002-01-05, by wenzelm
\newcommand{\isasymignore}{}, so we may use \<ignore> to disambiguate
2002-01-05, by wenzelm
tuned;
2002-01-05, by wenzelm
\hfootref: use \url markup;
2002-01-05, by wenzelm
more on concrete syntax;
2002-01-05, by wenzelm
fixed \index;
2002-01-05, by wenzelm
tuned ``syntax (output)'';
2002-01-04, by wenzelm
isatool document: stderr to stdout;
2002-01-04, by wenzelm
tuned;
2002-01-04, by wenzelm
document preparation overview;
2002-01-04, by wenzelm
beginnings of concrete syntax;
2002-01-04, by wenzelm
include typedef image without path prefix!
2002-01-04, by wenzelm
updated;
2002-01-04, by wenzelm
link Types/typedef images;
2002-01-04, by wenzelm
Isar version;
2002-01-03, by wenzelm
tuned msg;
2002-01-03, by wenzelm
\CONSTDEFS;
2002-01-03, by wenzelm
tuned;
2002-01-03, by wenzelm
next round of updates;
2002-01-03, by wenzelm
Some new theorems for ordinals
2002-01-03, by paulson
tuned;
2002-01-02, by wenzelm
first stage of major update;
2002-01-02, by wenzelm
added zf.tex;
2002-01-02, by wenzelm