2002-02-21 |
wenzelm |
updated title;
|
changeset |
files
|
2002-02-21 |
kleing |
new MicroJava document
|
changeset |
files
|
2002-02-21 |
kleing |
fix toc
|
changeset |
files
|
2002-02-21 |
wenzelm |
fixed document;
|
changeset |
files
|
2002-02-21 |
wenzelm |
tr: quote argument;
|
changeset |
files
|
2002-02-21 |
kleing |
new document
|
changeset |
files
|
2002-02-20 |
berghofe |
Removed superfluous lookup of theorems in Relation.thy
|
changeset |
files
|
2002-02-20 |
berghofe |
Moved change_type to proofterm.ML
|
changeset |
files
|
2002-02-20 |
berghofe |
New function strip_comb (cterm version of Term.strip_comb).
|
changeset |
files
|
2002-02-20 |
berghofe |
New function change_type for changing type assignments of theorems,
|
changeset |
files
|
2002-02-20 |
berghofe |
New function for eliminating definitions in proof term.
|
changeset |
files
|
2002-02-20 |
berghofe |
Converted to new theory format.
|
changeset |
files
|
2002-02-19 |
wenzelm |
added is_quasi;
|
changeset |
files
|
2002-02-19 |
wenzelm |
removed obscure functions bump_int_list, bump_list, bump_string;
|
changeset |
files
|
2002-02-19 |
wenzelm |
Symbol.bump_string;
|
changeset |
files
|
2002-02-19 |
wenzelm |
tuned;
|
changeset |
files
|
2002-02-19 |
wenzelm |
Paulson:1989;
|
changeset |
files
|
2002-02-19 |
wenzelm |
"isatool usedir -D output HOL Test && isatool document Test/output";
|
changeset |
files
|
2002-02-16 |
kleing |
fixed copy_all
|
changeset |
files
|
2002-02-16 |
wenzelm |
converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy);
|
changeset |
files
|
2002-02-15 |
wenzelm |
removed unused unmask_interrupt;
|
changeset |
files
|
2002-02-15 |
wenzelm |
clarified copy_all;
|
changeset |
files
|
2002-02-15 |
wenzelm |
moved copy_all to Thy/present.ML;
|
changeset |
files
|
2002-02-15 |
wenzelm |
replaced nodups by distinct;
|
changeset |
files
|
2002-02-15 |
wenzelm |
tuned;
|
changeset |
files
|
2002-02-15 |
paulson |
a new definition of "restrict"
|
changeset |
files
|
2002-02-14 |
wenzelm |
made MLWorks happy;
|
changeset |
files
|
2002-02-14 |
nipkow |
*** empty log message ***
|
changeset |
files
|
2002-02-14 |
nipkow |
nodups -> distinct
|
changeset |
files
|
2002-02-14 |
nipkow |
nodups -> distinct
|
changeset |
files
|
2002-02-13 |
paulson |
deleted some redundant 'addS*Es [equalityC*E]'s
|
changeset |
files
|
2002-02-13 |
paulson |
new function lemmas
|
changeset |
files
|
2002-02-13 |
paulson |
tidied. no more special simpset (super_ss)
|
changeset |
files
|
2002-02-13 |
paulson |
new lemmas for closure under Union
|
changeset |
files
|
2002-02-12 |
wenzelm |
eliminated Pure/Isar/comment.ML;
|
changeset |
files
|
2002-02-12 |
wenzelm |
ANTIQUOTE_FAIL;
|
changeset |
files
|
2002-02-12 |
wenzelm |
eliminated Isar/comment.ML;
|
changeset |
files
|
2002-02-12 |
wenzelm |
tuned;
|
changeset |
files
|
2002-02-12 |
wenzelm |
added isabelle-hol-book;
|
changeset |
files
|
2002-02-12 |
wenzelm |
* Isar/Pure: marginal comments ``--'' may now occur just anywhere in the text;
|
changeset |
files
|
2002-02-12 |
wenzelm |
got rid of explicit marginal comments (now stripped earlier from input);
|
changeset |
files
|
2002-02-12 |
wenzelm |
tuned;
|
changeset |
files
|
2002-02-11 |
wenzelm |
ML-Systems/smlnj-compiler.ML compatibility tweak;
|
changeset |
files
|
2002-02-11 |
wenzelm |
include SVC_Test;
|
changeset |
files
|
2002-02-07 |
berghofe |
Theorems are only "pre-named" if the do not already have names.
|
changeset |
files
|
2002-02-06 |
berghofe |
Added function could_unify to speed up rewriting of proof terms.
|
changeset |
files
|
2002-02-06 |
berghofe |
Indexes of variables in expanded proofs are now incremented to avoid clashes.
|
changeset |
files
|
2002-02-05 |
wenzelm |
moved SVC stuff to ex;
|
changeset |
files
|
2002-02-05 |
berghofe |
New function maxidx_of_proof.
|
changeset |
files
|
2002-02-04 |
paulson |
New-style versions of these old examples
|
changeset |
files
|
2002-02-02 |
berghofe |
Rewrite procedure now works for both compact and full proof objects.
|
changeset |
files
|
2002-01-30 |
wenzelm |
escape_mfix;
|
changeset |
files
|
2002-01-30 |
wenzelm |
added literal;
|
changeset |
files
|
2002-01-30 |
wenzelm |
prep_mixfix': proper use of Syntax.literal;
|
changeset |
files
|
2002-01-30 |
wenzelm |
tuned;
|
changeset |
files
|
2002-01-30 |
paulson |
mu-syntax for the LEAST operator
|
changeset |
files
|
2002-01-30 |
paulson |
Multiset: added the translation Mult(A) => A-||>nat-{0}
|
changeset |
files
|
2002-01-28 |
wenzelm |
tuned;
|
changeset |
files
|
2002-01-28 |
wenzelm |
GPLed;
|
changeset |
files
|
2002-01-28 |
wenzelm |
tuned header;
|
changeset |
files
|
2002-01-28 |
wenzelm |
tuned;
|
changeset |
files
|
2002-01-28 |
schirmer |
Bali added
|
changeset |
files
|
2002-01-28 |
schirmer |
Isabelle/Bali sources;
|
changeset |
files
|
2002-01-26 |
wenzelm |
Isar cases/induct: no backtracking;
|
changeset |
files
|
2002-01-26 |
wenzelm |
cases: really append cases_default;
|
changeset |
files
|
2002-01-26 |
wenzelm |
generic DETERM;
|
changeset |
files
|
2002-01-25 |
paulson |
ZF
|
changeset |
files
|
2002-01-24 |
wenzelm |
copy_files *.sty;
|
changeset |
files
|
2002-01-24 |
wenzelm |
cond_print_result_rule: priority (again) instead of slightly
|
changeset |
files
|
2002-01-24 |
wenzelm |
fixed subgoal_tac; fails on non-existent subgoal;
|
changeset |
files
|
2002-01-24 |
wenzelm |
copy_styles replaces overly conservative update_styles;
|
changeset |
files
|
2002-01-24 |
wenzelm |
Springer LNCS 2283;
|
changeset |
files
|
2002-01-24 |
wenzelm |
updated;
|
changeset |
files
|
2002-01-24 |
wenzelm |
iff del: less_Suc0 -- luckily this does NOT affect the printed text;
|
changeset |
files
|
2002-01-23 |
wenzelm |
delsimps [less_Suc0];
|
changeset |
files
|
2002-01-23 |
wenzelm |
less_Suc0;
|
changeset |
files
|
2002-01-23 |
wenzelm |
error "Unexpected end of input";
|
changeset |
files
|
2002-01-23 |
wenzelm |
reorganized code for predicate text;
|
changeset |
files
|
2002-01-23 |
wenzelm |
tuned;
|
changeset |
files
|
2002-01-23 |
wenzelm |
* HOL: nat_number_of;
|
changeset |
files
|
2002-01-23 |
paulson |
A few more standard simprules, TCs, etc.
|
changeset |
files
|
2002-01-22 |
wenzelm |
qualified_result replaces qualified;
|
changeset |
files
|
2002-01-22 |
wenzelm |
added locale_facts(_i) interface (useful for simple ML proof tools);
|
changeset |
files
|
2002-01-21 |
wenzelm |
full_proofs;
|
changeset |
files
|
2002-01-21 |
wenzelm |
* Pure/show_hyps reset by default (in accordance to existing Isar practice);
|
changeset |
files
|
2002-01-21 |
wenzelm |
reset show_hyps by default (in accordance to existing Isar practice);
|
changeset |
files
|
2002-01-21 |
wenzelm |
save library;
|
changeset |
files
|
2002-01-21 |
wenzelm |
full_atomize;
|
changeset |
files
|
2002-01-21 |
wenzelm |
wild guess at polyml-4.1.2;
|
changeset |
files
|
2002-01-21 |
wenzelm |
options -l and -t;
|
changeset |
files
|
2002-01-21 |
berghofe |
Removed timing function.
|
changeset |
files
|
2002-01-21 |
paulson |
new simprules and classical rules
|
changeset |
files
|
2002-01-21 |
berghofe |
Tuned name mangling function.
|
changeset |
files
|
2002-01-21 |
berghofe |
Made some proofs constructive.
|
changeset |
files
|
2002-01-21 |
berghofe |
datatype_codegen now checks type of constructor.
|
changeset |
files
|
2002-01-21 |
nipkow |
*** empty log message ***
|
changeset |
files
|
2002-01-21 |
paulson |
lexical tidying
|
changeset |
files
|
2002-01-21 |
paulson |
slight re-use of code
|
changeset |
files
|
2002-01-19 |
kleing |
fixed typos
|
changeset |
files
|
2002-01-18 |
wenzelm |
rewrite_term: removed rew0, so no on-the-fly eta-contraction;
|
changeset |
files
|
2002-01-18 |
wenzelm |
fixed document setup of HOL-Library;
|
changeset |
files
|
2002-01-18 |
wenzelm |
tuned;
|
changeset |
files
|
2002-01-18 |
paulson |
tidied
|
changeset |
files
|
2002-01-18 |
paulson |
OOPS
|
changeset |
files
|
2002-01-18 |
paulson |
tweaks
|
changeset |
files
|
2002-01-18 |
wenzelm |
moved document sources to proper place, *within* Library/Library (!);
|
changeset |
files
|
2002-01-17 |
wenzelm |
cover polyml-4.1.2;
|
changeset |
files
|
2002-01-17 |
wenzelm |
RuleCases.make interface based on term instead of thm;
|
changeset |
files
|
2002-01-17 |
wenzelm |
RuleCases.make interface based on term instead of thm;
|
changeset |
files
|
2002-01-17 |
wenzelm |
atomize_term replaces atomize_cterm;
|
changeset |
files
|
2002-01-17 |
wenzelm |
ObjectLogic.atomize_term replaces ObjectLogic.atomize_cterm;
|
changeset |
files
|
2002-01-17 |
wenzelm |
Thm.prop_of;
|
changeset |
files
|
2002-01-17 |
wenzelm |
Tactic.norm_hhf renamed to Tactic.norm_hhf_rule;
|
changeset |
files
|
2002-01-17 |
wenzelm |
added prop_of: thm -> term (at last!);
|
changeset |
files
|
2002-01-17 |
wenzelm |
added add_term_free_names (more precise/efficient than add_term_names);
|
changeset |
files
|
2002-01-17 |
wenzelm |
renamed norm_hhf to norm_hhf_rule;
|
changeset |
files
|
2002-01-17 |
wenzelm |
added is_norm_hhf (from logic.ML);
|
changeset |
files
|
2002-01-17 |
wenzelm |
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
|
changeset |
files
|
2002-01-17 |
wenzelm |
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
|
changeset |
files
|
2002-01-17 |
wenzelm |
eta_contract with sharing (by berghofe);
|
changeset |
files
|