Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
solved the problem that Larry's simproce cancle_numerals(?) returns
2002-02-25, by nipkow
added using_thmss(_i);
2002-02-24, by wenzelm
added using_facts;
2002-02-24, by wenzelm
replaced 'using' keyword by 'to';
2002-02-24, by wenzelm
tuned;
2002-02-24, by wenzelm
'using' command;
2002-02-24, by wenzelm
Added check for field/method access to operational semantics and proved the acesses valid.
2002-02-22, by schirmer
* HOL: removed obsolete theorem "optionE";
2002-02-21, by wenzelm
fixed get_name_tags in order to work with hyps;
2002-02-21, by wenzelm
clarified internal theory dependencies;
2002-02-21, by wenzelm
bind_thms basic_monos;
2002-02-21, by wenzelm
include theory Record (tuned dependencies);
2002-02-21, by wenzelm
removed theory Option;
2002-02-21, by wenzelm
theory Option has been assimilated by Datatype;
2002-02-21, by wenzelm
* HOL: removed obsolete theorem "optionE";
2002-02-21, by wenzelm
updated title;
2002-02-21, by wenzelm
new MicroJava document
2002-02-21, by kleing
fix toc
2002-02-21, by kleing
fixed document;
2002-02-21, by wenzelm
tr: quote argument;
2002-02-21, by wenzelm
new document
2002-02-21, by kleing
Removed superfluous lookup of theorems in Relation.thy
2002-02-20, by berghofe
Moved change_type to proofterm.ML
2002-02-20, by berghofe
New function strip_comb (cterm version of Term.strip_comb).
2002-02-20, by berghofe
New function change_type for changing type assignments of theorems,
2002-02-20, by berghofe
New function for eliminating definitions in proof term.
2002-02-20, by berghofe
Converted to new theory format.
2002-02-20, by berghofe
added is_quasi;
2002-02-20, by wenzelm
removed obscure functions bump_int_list, bump_list, bump_string;
2002-02-20, by wenzelm
Symbol.bump_string;
2002-02-20, by wenzelm
tuned;
2002-02-19, by wenzelm
Paulson:1989;
2002-02-19, by wenzelm
"isatool usedir -D output HOL Test && isatool document Test/output";
2002-02-19, by wenzelm
fixed copy_all
2002-02-16, by kleing
converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy);
2002-02-16, by wenzelm
removed unused unmask_interrupt;
2002-02-15, by wenzelm
clarified copy_all;
2002-02-15, by wenzelm
moved copy_all to Thy/present.ML;
2002-02-15, by wenzelm
replaced nodups by distinct;
2002-02-15, by wenzelm
tuned;
2002-02-15, by wenzelm
a new definition of "restrict"
2002-02-15, by paulson
made MLWorks happy;
2002-02-14, by wenzelm
*** empty log message ***
2002-02-14, by nipkow
nodups -> distinct
2002-02-14, by nipkow
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
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
added isabelle-intro, isabelle-logics;
2002-01-02, by wenzelm
added \indexisarcmdof, \indexisarmethof, \indexisarattof;
2002-01-02, by wenzelm
New theorems by Sidi Ehmety
2002-01-02, by paulson
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
2002-01-02, by paulson
Added "Executing higher order logic" paper.
2001-12-31, by berghofe
Added section on code generator.
2001-12-31, by berghofe
tuned document sources;
2001-12-29, by wenzelm
'inductive_cases': support 'and' form;
2001-12-29, by wenzelm
* ZF/IMP: updated and converted to new-style theory format;
2001-12-29, by wenzelm
update by Stephan Merz;
2001-12-29, by wenzelm
conversion to Isar/ZF
2001-12-28, by paulson
fixed variable-clash bug in make_elim
2001-12-28, by paulson
obsolete;
2001-12-27, by wenzelm
tuned tracing markup;
2001-12-27, by wenzelm
tuned tracing_fn markup;
2001-12-27, by wenzelm
solve rule: tracing instead of priority;
2001-12-27, by wenzelm
tuned;
2001-12-27, by wenzelm
IMP/document/root.tex;
2001-12-27, by wenzelm
warn for spaces in ISABELLE_HOME;
2001-12-27, by wenzelm
HOL/IMP and HOLCF/IMP updated and converted (Gerwin Klein);
2001-12-27, by wenzelm
some new theorems
2001-12-25, by paulson
conversion to Isar
2001-12-25, by paulson
tweaked the standard theorems
2001-12-22, by paulson
Resid converted to Isar/ZF
2001-12-22, by paulson
restart: sync_thy_loader instead of overly aggressive touch_all_thys;
2001-12-21, by wenzelm
qualified point.more;
2001-12-21, by wenzelm
hide base name of "make", "fields", "extend", "truncate", "more",
2001-12-21, by wenzelm
Theory.hide_space_i true;
2001-12-21, by wenzelm
hide: flag for full/base name;
2001-12-21, by wenzelm
HOL/record: shared operations ("more", "fields", etc.) now need to be
2001-12-21, by wenzelm
tuned;
2001-12-21, by wenzelm
updated;
2001-12-21, by wenzelm
updated;
2001-12-21, by wenzelm
isatool browser -o;
2001-12-21, by wenzelm
removed Misc/Translations (text covered by Documents.thy);
2001-12-21, by wenzelm
Redundant patterns no longer cause errors.
2001-12-21, by berghofe
Code generator now adds type constraints to val declarations (to make
2001-12-21, by berghofe
tuned;
2001-12-21, by wenzelm
updated;
2001-12-21, by wenzelm
removed Types/records.tex;
2001-12-21, by wenzelm
added add_fixes: derives mssing type scheme from mixfix;
2001-12-21, by wenzelm
fixed inst_thm: proper domain of env;
2001-12-21, by wenzelm
tuned;
2001-12-21, by wenzelm
added lemma;
2001-12-20, by wenzelm
generated text;
2001-12-20, by wenzelm
supplanted by Records.thy;
2001-12-20, by wenzelm
some text;
2001-12-20, by wenzelm
\usepackage{marvosym};
2001-12-20, by wenzelm
document/Records.tex;
2001-12-20, by wenzelm
turned into proper Isabelle document;
2001-12-20, by wenzelm
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
2001-12-20, by nipkow
Eliminated "query" syntax.
2001-12-20, by berghofe
*** empty log message ***
2001-12-20, by nipkow
ZF/Main
2001-12-20, by paulson
Fixed bug in function add.
2001-12-20, by berghofe
new hfootref macro for Web links
2001-12-20, by paulson
converted some ZF/Induct examples to Isar
2001-12-20, by paulson
cast_ok and match_exception_entry no longer disabled (thanks to
2001-12-20, by berghofe
cast_ok no longer disabled (thanks to improvement of code generator).
2001-12-20, by berghofe
Implemented higher order modes.
2001-12-20, by berghofe
Moved "code" attribute to Pure/codegen.ML
2001-12-20, by berghofe
"code" attribute is now managed by basic code generator module.
2001-12-20, by berghofe
Declared characteristic equations for < on nat for code generation.
2001-12-20, by berghofe
*** empty log message ***
2001-12-19, by nipkow
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
2001-12-19, by paulson
hyperlinks in DVI mode
2001-12-19, by paulson
generalize type variables properly: start with occurrences in objects
2001-12-19, by wenzelm
tuned interface of ProofContext.generalize;
2001-12-19, by wenzelm
HOL/IMP: include session graph;
2001-12-19, by wenzelm
updated;
2001-12-19, by wenzelm
tuned;
2001-12-19, by wenzelm
removed preallocated heaps axiom (now in type safety invariant)
2001-12-18, by kleing
updated;
2001-12-18, by wenzelm
New type definition diagram
2001-12-18, by paulson
added exec_lub
2001-12-18, by nipkow
new type definition figure
2001-12-18, by paulson
minor suggestions from Markus
2001-12-18, by paulson
additional material
2001-12-18, by paulson
* system: tested support for MacOS X;
2001-12-18, by wenzelm
better simplification makes steps redundant
2001-12-18, by paulson
replaced lepoll_lesspoll_lesspoll, lesspoll_lepoll_lesspoll
2001-12-18, by paulson
tuned;
2001-12-18, by wenzelm
use Locale.read/cert_context_statement;
2001-12-18, by wenzelm
*** empty log message ***
2001-12-18, by nipkow
tuned;
2001-12-18, by wenzelm
improved mixfix_args;
2001-12-18, by wenzelm
tuned Type.unify;
2001-12-18, by wenzelm
simultaneous type-inference of complete context/statement specifications;
2001-12-18, by wenzelm
tuned interface of unify, param;
2001-12-18, by wenzelm
tuned Type.unify;
2001-12-18, by wenzelm
mods due to changed 1-point simprocs (quantifier1).
2001-12-17, by nipkow
mods due to improved 1-point simprocs (quantifier1).
2001-12-17, by nipkow
mods due to mor powerful simprocs for 1-point rules (quantifier1).
2001-12-17, by nipkow
now permutations of quantifiers are allowed as well.
2001-12-17, by nipkow
fixed JVMListExample
2001-12-17, by kleing
MicroJava exception merge
2001-12-16, by kleing
temporarily removed JVMListExample
2001-12-16, by kleing
exception merge + cleanup
2001-12-16, by kleing
exception merge, doesn't work yet
2001-12-16, by kleing
exception merge, cleanup, tuned
2001-12-16, by kleing
exceptions
2001-12-16, by kleing
list_all2_rev
2001-12-16, by kleing
removed debug stuff;
2001-12-14, by wenzelm
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
2001-12-14, by wenzelm
removed special treatment of "_" in syntax (now covered by \<index> arg);
2001-12-14, by wenzelm
tuned locale interface;
2001-12-14, by wenzelm
proper treatment of internal parameters;
2001-12-14, by wenzelm
\usepackage[latin1]{inputenc};
2001-12-14, by wenzelm
Wenzel:2001:Isar-examples;
2001-12-14, by wenzelm
updated;
2001-12-14, by wenzelm
mixfix syntax for selectors;
2001-12-14, by wenzelm
record: mixfix;
2001-12-14, by wenzelm
export used_types;
2001-12-14, by wenzelm
Locale.activate_context;
2001-12-14, by wenzelm
beginning support for type instantiation;
2001-12-14, by wenzelm
varify returns newly introduced variables;
2001-12-14, by wenzelm
varifyT' returns newly introduces variables;
2001-12-14, by wenzelm
added invent_type_names;
2001-12-14, by wenzelm
changed Thm.varifyT';
2001-12-14, by wenzelm
type_env;
2001-12-14, by wenzelm
added type_env function;
2001-12-14, by wenzelm
export add_tvarsT etc.;
2001-12-14, by wenzelm
changed Type.varify;
2001-12-14, by wenzelm
Term.invent_type_names;
2001-12-14, by wenzelm
*** empty log message ***
2001-12-13, by nipkow
*** empty log message ***
2001-12-13, by nipkow
made SML/XL happy;
2001-12-13, by wenzelm
*** empty log message ***
2001-12-13, by nipkow
Terminator now uses arith_tac as well.
2001-12-13, by nipkow
comp -> rel_comp
2001-12-13, by nipkow
isatool expandshort;
2001-12-13, by wenzelm
Relaxed the precondition of UN_upper_le
2001-12-13, by paulson
isatool expandshort;
2001-12-12, by wenzelm
new rewrite rules for use by arith_tac to take care of uminus.
2001-12-12, by nipkow
new rewrite rules for use by arith_tac to take care of uminus.
2001-12-12, by nipkow
mods due to reorienting and renaming of real_minus_mult_eq1/2
2001-12-12, by nipkow
tuned conversion from terms to "polynomials" for arith_tac: takes care
2001-12-12, by nipkow
drop_judgment: be graceful about undeclared judgment;
2001-12-12, by wenzelm
obsolete;
2001-12-12, by wenzelm
option "-d pdf" by default (accomodates pdf bias of Mac OS X);
2001-12-12, by wenzelm
removed installfonts, xterm interface;
2001-12-12, by wenzelm
Removed pointless backtracking from arith_tac
2001-12-12, by nipkow
Improved error messages.
2001-12-12, by berghofe
*** empty log message ***
2001-12-12, by nipkow
tuned;
2001-12-11, by wenzelm
obsolete;
2001-12-11, by wenzelm
obsolete;
2001-12-11, by wenzelm
tuned;
2001-12-11, by wenzelm
\isasymindex made text mode;
2001-12-11, by wenzelm
isatools "symbolinput" and "nonascii" have disappeared;
2001-12-11, by wenzelm
added HOL-Library;
2001-12-11, by wenzelm
tuned;
2001-12-11, by wenzelm
updated;
2001-12-11, by wenzelm
removed altogether;
2001-12-11, by wenzelm
removed unused stuff;
2001-12-11, by wenzelm
Updated.
2001-12-11, by berghofe
oops;
2001-12-11, by wenzelm
bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
2001-12-10, by wenzelm
updated reserved words of HOL;
2001-12-10, by wenzelm
* HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead
2001-12-10, by wenzelm
obsolete;
2001-12-10, by wenzelm
removed additional blank line (confuses some versions of make);
2001-12-10, by wenzelm
obsolete;
2001-12-10, by wenzelm
- Changed type of invoke_codegen
2001-12-10, by berghofe
- Added code generator interface for types
2001-12-10, by berghofe
less
more
|
(0)
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip