Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-1920
+1920
+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.
moved add_axioms_x, add_defs_x to Isar/isar_thy.ML;
1998-06-10, by wenzelm
added exnMessage;
1998-06-10, by wenzelm
added General;
1998-06-10, by wenzelm
added of_file;
1998-06-10, by wenzelm
General tools.
1998-06-10, by wenzelm
moved table.ML, object.ML, seq.ML, name_space.ML to General;
1998-06-10, by wenzelm
moved object.ML to General/object.ML;
1998-06-10, by wenzelm
moved table.ML to General/table.ML;
1998-06-10, by wenzelm
moved seq.ML to General/seq.ML;
1998-06-10, by wenzelm
moved position.ML, path.ML, file.ML to General;
1998-06-10, by wenzelm
moved name_space.ML to General/name_space.ML;
1998-06-10, by wenzelm
moved Thy/path.ML to General/path.ML;
1998-06-10, by wenzelm
moved Thy/position.ML to General/position.ML;
1998-06-10, by wenzelm
moved Thy/file.ML to General/file.ML;
1998-06-10, by wenzelm
new type-safe user interface for theory data;
1998-06-10, by wenzelm
nonterminals prog;
1998-06-09, by wenzelm
adapted to new theory data interface;
1998-06-09, by wenzelm
use type-safe theory data interface;
1998-06-08, by wenzelm
added theory_data.ML;
1998-06-08, by wenzelm
Type-safe interface for theory data.
1998-06-08, by wenzelm
* improved the theory data mechanism to support real encapsulation;
1998-06-05, by wenzelm
accomodate tuned version of theory data;
1998-06-05, by wenzelm
added print_theorems: theory -> unit;
1998-06-05, by wenzelm
Object.T;
1998-06-05, by wenzelm
improved data: secure version using Object.T and Object.kind;
1998-06-05, by wenzelm
tuned setup;
1998-06-05, by wenzelm
use Object.T and Object.kind;
1998-06-05, by wenzelm
removed type object (see object.ML);
1998-06-05, by wenzelm
tuned print_exn;
1998-06-05, by wenzelm
print_data moved to theory.ML;
1998-06-05, by wenzelm
added THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq;
1998-06-05, by wenzelm
added object.ML;
1998-06-05, by wenzelm
added option_map_o_empty
1998-06-02, by oheimb
added split_etas
1998-06-02, by oheimb
added split_sum_case_asm
1998-06-02, by oheimb
tuned;
1998-05-29, by wenzelm
tuned msgs;
1998-05-29, by wenzelm
auto update
1998-05-28, by paulson
fixed ml_prompts;
1998-05-28, by wenzelm
changed get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option;
1998-05-28, by wenzelm
tuned dist version;
1998-05-28, by wenzelm
tuned header;
1998-05-28, by wenzelm
version under control of Admin/makedist;
1998-05-28, by wenzelm
README, Pure/ROOT.ML: version set automatically;
1998-05-28, by wenzelm
version under control of Admin/makedist;
1998-05-28, by wenzelm
added ml_prompts;
1998-05-28, by wenzelm
added mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c)
1998-05-28, by wenzelm
tuned error msg;
1998-05-28, by wenzelm
fixed error msgs;
1998-05-28, by wenzelm
Structure Option now declared in MLWorks
1998-05-27, by paulson
mk_all_imp: no longer creates goals that have beta-redexes
1998-05-27, by paulson
more tracing
1998-05-27, by paulson
Changed require to requires for MLWorks
1998-05-27, by paulson
auto update
1998-05-27, by paulson
made SML/NJ happy;
1998-05-26, by wenzelm
foldl_map prep_field;
1998-05-26, by wenzelm
tuned store_theory;
1998-05-25, by wenzelm
tuned local, global;
1998-05-25, by wenzelm
tuned store_theory: theory -> unit;
1998-05-25, by wenzelm
added get_name, put_name, global_path, local_path, begin_theory,
1998-05-25, by wenzelm
global_names moved to pure_thy.ML;
1998-05-25, by wenzelm
certify_term: type_check replaces Term.type_of, providing sensible
1998-05-25, by wenzelm
renamed state_source to source';
1998-05-25, by wenzelm
added recover, source;
1998-05-25, by wenzelm
added catch: ('a -> 'b) -> 'a -> 'b;
1998-05-25, by wenzelm
remove seq2, scan (use seq2, foldl_map from library.ML);
1998-05-25, by wenzelm
added foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list;
1998-05-25, by wenzelm
Swapped order of params.
1998-05-25, by nipkow
changed get_single: ('a, 'b) source -> 'a option * ('a, 'b) source;
1998-05-20, by wenzelm
source vs. source';
1998-05-20, by wenzelm
tuned keywords;
1998-05-20, by wenzelm
added is_stale;
1998-05-20, by wenzelm
tuned signature;
1998-05-20, by wenzelm
tuned comments;
1998-05-20, by wenzelm
tuned;
1998-05-20, by wenzelm
Small mods.
1998-05-20, by nipkow
prompt made part of source;
1998-05-19, by wenzelm
fixed handle_error: cat_lines;
1998-05-19, by wenzelm
added Thy/position.ML;
1998-05-19, by wenzelm
added source: string -> (string, string list) Source.source;
1998-05-19, by wenzelm
Input positions.
1998-05-19, by wenzelm
added Syntax/source.ML;
1998-05-18, by wenzelm
added Source module;
1998-05-18, by wenzelm
Co-algebraic data sources.
1998-05-18, by wenzelm
Symbol.stopper;
1998-05-18, by wenzelm
improved finite scans: more abstract stopper;
1998-05-18, by wenzelm
snoc_induct/exhaust -> rev_induct_exhaust.
1998-05-18, by nipkow
Cleaned up and simplified etc.
1998-05-18, by nipkow
witnesses: lookup stored thms instead of axioms;
1998-05-15, by wenzelm
added add_axioms_x, add_defs_x;
1998-05-15, by wenzelm
PureThy.add_typedecls;
1998-05-15, by wenzelm
Reordred arguments in AutoChopper.
1998-05-14, by nipkow
extended addsplits and delsplits to handle also split rules for assumptions
1998-05-14, by oheimb
simplifications
1998-05-14, by oheimb
disabled (experimental) geometry option
1998-05-14, by oheimb
keyboard settings now done by loading Tools/8bit/xemacs/isa_xemacs.emacs
1998-05-14, by oheimb
added option_map_o_update
1998-05-14, by oheimb
added welcome;
1998-05-13, by wenzelm
added :-- (dependent pair);
1998-05-13, by wenzelm
added transform_error, exception ERROR_MESSAGE;
1998-05-13, by wenzelm
added thms_closure: theory -> xstring -> tthm list option;
1998-05-13, by wenzelm
adapted to new Scan.fail_with / Scan.!!;
1998-05-13, by wenzelm
pure_nonterms;
1998-05-13, by wenzelm
added fail_with and adapted !!;
1998-05-13, by wenzelm
gen_attr: fixed order of evaluation;
1998-05-13, by wenzelm
tuned msg;
1998-05-13, by wenzelm
get_first: ('a -> 'b option) -> 'a list -> 'b option;
1998-05-13, by wenzelm
HOL/record: now includes concrete syntax for record terms;
1998-05-13, by wenzelm
added Goal, Goalw;
1998-05-12, by wenzelm
branching_level = 250;
1998-05-12, by wenzelm
fixed comment;
1998-05-12, by wenzelm
Removed duplicate list_length_induct
1998-05-12, by nipkow
Reordered a few parameters.
1998-05-11, by nipkow
Lex
1998-05-11, by nipkow
tuned comment;
1998-05-10, by wenzelm
Reshuffeling, renaming and a few simple corollaries.
1998-05-08, by nipkow
fixed translations;
1998-05-08, by wenzelm
proper thy files;
1998-05-08, by wenzelm
fixed update syntax;
1998-05-08, by wenzelm
improved source: state-based;
1998-05-07, by wenzelm
added scan_tvar;
1998-05-07, by wenzelm
added 'space';
1998-05-07, by wenzelm
Got rid of NAe.delta
1998-05-07, by nipkow
HOL/Update
1998-05-06, by paulson
Removed some traces of UNITY
1998-05-06, by paulson
Changed [/] to [:=] and removed actual definition.
1998-05-06, by nipkow
New syntax for function update; moved to main HOL directory
1998-05-05, by paulson
misc tuning;
1998-05-05, by wenzelm
'more' selector;
1998-05-04, by wenzelm
added nth_update: 'a -> int * 'a list -> 'a list;
1998-05-04, by wenzelm
tuned msg;
1998-05-04, by wenzelm
fixed constdefs syntax;
1998-05-04, by wenzelm
concrete syntax for record terms;
1998-05-04, by wenzelm
New behaviour of asm_full_simp_tac.
1998-05-04, by nipkow
added CLASIMPSET(') tacticals;
1998-05-02, by wenzelm
added trfun_names;
1998-05-02, by wenzelm
added accesses: string -> string list;
1998-05-02, by wenzelm
minor corrections
1998-05-01, by oheimb
Auto_tac: now uses enhanced version of asm_full_simp_tac,
1998-05-01, by oheimb
added finite_dom_map_of and ran_update
1998-05-01, by oheimb
added insert_Collect
1998-05-01, by oheimb
corrected and updated description of wrapper mechanism (including addss)
1998-05-01, by oheimb
*** empty log message ***
1998-05-01, by nipkow
"let" is no longer restricted to FOL terms and allows any logical terms
1998-05-01, by paulson
Let.ML and Let.thy had been omitted
1998-05-01, by paulson
fixed simpset(), claset();
1998-04-30, by wenzelm
moved records data to Tools/record_package.ML;
1998-04-29, by wenzelm
nontermials;
1998-04-29, by wenzelm
Theory.require;
1998-04-29, by wenzelm
TypedefPackage.add_typedef;
1998-04-29, by wenzelm
Theory.require;
1998-04-29, by wenzelm
Logic.mk_defpair;
1998-04-29, by wenzelm
Extensible records with structural subtyping in HOL. See
1998-04-29, by wenzelm
new theory section 'setup';
1998-04-29, by wenzelm
nonterminals;
1998-04-29, by wenzelm
package extensible records with structural subtyping in HOL -- still
1998-04-29, by wenzelm
renamed from typedef.ML;
1998-04-29, by wenzelm
reworked and moved to Tools/record_package.ML;
1998-04-29, by wenzelm
removed typedef.ML, record.ML;
1998-04-29, by wenzelm
renamed to Tools/typedef_package.ML;
1998-04-29, by wenzelm
adapted to new PureThy.add_axioms_i;
1998-04-29, by wenzelm
adapted to new PureThy.add_tthmss;
1998-04-29, by wenzelm
Theory.require;
1998-04-29, by wenzelm
adapted to new PureThy.add_axioms;
1998-04-29, by wenzelm
new theory section 'nonterminals';
1998-04-29, by wenzelm
adapted to new PureThy.add_defs;
1998-04-29, by wenzelm
Theory.require;
1998-04-29, by wenzelm
tuned setup;
1998-04-29, by wenzelm
tuned setup;
1998-04-29, by wenzelm
tuned names of (add_)store_XXX functions;
1998-04-29, by wenzelm
replaced thy_setup by 'setup' section;
1998-04-29, by wenzelm
added append;
1998-04-29, by wenzelm
added none: 'a -> 'a * 'b attribute list;
1998-04-29, by wenzelm
tuned error msgs;
1998-04-29, by wenzelm
moved mk_defpair to logic.ML;
1998-04-29, by wenzelm
tuned get_ax (uses ancestry);
1998-04-29, by wenzelm
renamed setup to apply;
1998-04-29, by wenzelm
adapted to new PureThy.add_axioms_i;
1998-04-29, by wenzelm
added defaultS: sg -> sort;
1998-04-29, by wenzelm
added thm, thms;
1998-04-29, by wenzelm
*** empty log message ***
1998-04-29, by wenzelm
new thms, really demos of the final coalgebra theorem
1998-04-28, by paulson
new thms image_0_left, image_Un_left, etc.
1998-04-28, by paulson
new thm mult_lt_mono1
1998-04-28, by paulson
cleanup for split_all_tac as wrapper in claset()
1998-04-27, by oheimb
removed wrong comment
1998-04-27, by oheimb
added option_map_eq_Some via AddIffs
1998-04-27, by oheimb
*** empty log message ***
1998-04-27, by nipkow
delsplits, Addsplits, Delsplits.
1998-04-27, by nipkow
Renamed expand_const -> split_const
1998-04-27, by nipkow
Added conversion of reg.expr. to automata.
1998-04-27, by nipkow
Renamed expand_const -> split_const.
1998-04-27, by nipkow
Added a few lemmas.
1998-04-27, by nipkow
New proof of apply_equality and new thm Pi_image_cons
1998-04-27, by paulson
improved split_all_tac significantly
1998-04-24, by oheimb
improved keyboard modifiers
1998-04-24, by oheimb
added ASCII translation of subseteq
1998-04-24, by oheimb
tidied; div & mod
1998-04-24, by paulson
*** empty log message ***
1998-04-24, by oheimb
added no_syn;
1998-04-22, by wenzelm
added mk_cond_defpair, mk_defpair;
1998-04-22, by wenzelm
Modifications due to improved simplifier.
1998-04-22, by nipkow
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
1998-04-22, by nipkow
improved pair_tac to call prune_params_tac afterwards
1998-04-21, by oheimb
split_all_tac is now added to claset() _before_ other safe tactics
1998-04-21, by oheimb
made proof of zmult_congruent2 more stable
1998-04-21, by oheimb
simplification of explicit theory usage and merges
1998-04-21, by oheimb
removed split_all_tac from claset() globally within IOA
1998-04-21, by oheimb
made modifications of the simpset() local
1998-04-21, by oheimb
layout improvement
1998-04-21, by oheimb
expandshort; new gcd_induct with inbuilt case analysis
1998-04-21, by paulson
Renamed mod_XXX_cancel to mod_XXX_self
1998-04-21, by paulson
New laws for mod
1998-04-20, by paulson
proving fib(gcd(m,n)) = gcd(fib m, fib n)
1998-04-20, by paulson
fixed comment;
1998-04-19, by wenzelm
Fixed bug in inductive sections to allow disjunctive premises;
1998-04-10, by paulson
bug fixes
1998-04-10, by paulson
can prove the empty relation to be WF
1998-04-10, by paulson
Fixed bug in inductive sections to allow disjunctive premises;
1998-04-10, by paulson
Clearer description of recdef, including use of {}
1998-04-09, by paulson
Simplified the syntax description; mentioned FOL vs HOL
1998-04-09, by paulson
*** empty log message ***
1998-04-07, by oheimb
replaced option_map_SomeD by option_map_eq_Some (RS iffD1)
1998-04-07, by oheimb
made split_all_tac as safe wrapper more defensive:
1998-04-07, by oheimb
no open Simplifier;
1998-04-04, by wenzelm
tuned fail;
1998-04-04, by wenzelm
type_error;
1998-04-04, by wenzelm
tuned comments;
1998-04-04, by wenzelm
no open Simplifier;
1998-04-04, by wenzelm
replaced thy_data by thy_setup;
1998-04-04, by wenzelm
type_error;
1998-04-04, by wenzelm
replaced thy_data by setup;
1998-04-04, by wenzelm
removed simple;
1998-04-04, by wenzelm
added triv_goal, rev_triv_goal (for Isar);
1998-04-04, by wenzelm
added Goal_def;
1998-04-04, by wenzelm
replaced thy_data by thy_setup;
1998-04-04, by wenzelm
added local_theory (for Isar);
1998-04-04, by wenzelm
tuned trace msgs;
1998-04-04, by wenzelm
tuned names;
1998-04-03, by wenzelm
added get_tthm(s), store_tthms(s);
1998-04-03, by wenzelm
tuned comments;
1998-04-03, by wenzelm
added attribute.ML;
1998-04-03, by wenzelm
Theorem tags and attributes.
1998-04-03, by wenzelm
UNITY
1998-04-03, by paulson
repaired incompatibility with new SML version by eta-expansion
1998-04-03, by oheimb
New target HOL-UNITY
1998-04-03, by paulson
New UNITY theory
1998-04-03, by paulson
Tidied proofs
1998-04-03, by paulson
Tidied proofs by getting rid of case_tac
1998-04-03, by paulson
improved \tt appearance of many ASCII special symbols like #
1998-04-03, by oheimb
split_all_tac now fails if there is nothing to split
1998-04-02, by oheimb
new theorems
1998-04-02, by paulson
changed if_bool_eq to if_bool_eq_conj
1998-04-02, by paulson
changed if_bool_eq to if_bool_eq_conj and added if_bool_eq_disj
1998-04-02, by paulson
New theorems card_Diff_le and card_insert_le; tidied
1998-04-02, by paulson
introduced functions for updating the wrapper lists
1998-04-02, by oheimb
*** empty log message ***
1998-04-02, by oheimb
merge_cs now also merges safe and unsafe wrappers
1998-03-30, by oheimb
generalized appearance of trancl_into_rtrancl and r_into_trancl
1998-03-30, by oheimb
adapted proof of finite_converse
1998-03-30, by oheimb
added wf_converse_trancl, adapted proof of wfrec
1998-03-30, by oheimb
added caveat
1998-03-30, by oheimb
added introduction and elimination rules for Univalent
1998-03-30, by oheimb
added Univalent_rel_pow
1998-03-30, by oheimb
removed superfluous use_thy
1998-03-30, by oheimb
removed superfluous translations
1998-03-30, by oheimb
added try, single, many;
1998-03-24, by wenzelm
added cproj', and therefore extended prj
1998-03-24, by oheimb
added cproj', and therefore extended prj
1998-03-24, by oheimb
improved checks
1998-03-24, by oheimb
added o2s
1998-03-24, by oheimb
added finite_acyclic_wf_converse: corrected 8bit chars
1998-03-24, by oheimb
added acyclicI
1998-03-24, by oheimb
added finite_acyclic_wf_converse
1998-03-24, by oheimb
more thms
1998-03-23, by paulson
inverse -> converse
1998-03-16, by paulson
inverse -> converse
1998-03-16, by paulson
re-ordered proofs
1998-03-16, by paulson
moved addsplits [expand_if] from HOL_basic_ss to HOL_ss;
1998-03-13, by wenzelm
renamed not1_or to disj_not1, not2_or to disj_not2
1998-03-12, by oheimb
improved coding of delWrapper and delSWrapper
1998-03-12, by oheimb
addloop: added warning in case of overwriting a looper
1998-03-12, by oheimb
Made mutual simplification of prems a special case.
1998-03-12, by nipkow
Used merge_alists for loopers.
1998-03-12, by nipkow
New, stronger rewrites
1998-03-12, by paulson
The theorem nat_neqE, and some tidying
1998-03-12, by paulson
New laws, mostly generalizing old "pred" ones
1998-03-12, by paulson
spy_analz_tac now handles individual conjuncts properly
1998-03-11, by paulson
new theorem
1998-03-11, by paulson
New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
1998-03-11, by paulson
Arith.thy -> thy; proved a few new theorems
1998-03-11, by paulson
New Asm_full_simp_tac shortens proof.
1998-03-11, by nipkow
Simplifier
1998-03-11, by nipkow
More Lex.
1998-03-11, by nipkow
New Asm_full_simp_tac led to a loop.
1998-03-11, by nipkow
Mod because of new simplifier.
1998-03-10, by nipkow
Mod because of not1_or.
1998-03-10, by nipkow
Updated proofs because of new simplifier.
1998-03-10, by nipkow
Updated proofs because of new simplification tactics.
1998-03-10, by nipkow
Adapted proofs because of new simplification tactics.
1998-03-10, by nipkow
The new asm_lr_simp_tac is the old asm_full_simp_tac.
1998-03-10, by nipkow
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
1998-03-10, by oheimb
added not1_or and if_eq_cancel to simpset()
1998-03-10, by oheimb
added not1_or and if_eq_cancel to simpset()
1998-03-10, by oheimb
new rewrite rules not1_or, not2_or, and if_eq_cancel
1998-03-10, by oheimb
renamed smart_tac to force_tac, slight improvement of force_tac
1998-03-10, by oheimb
Asm_full_simp_tac now reorients asm c = t to t = c.
1998-03-10, by nipkow
adhoc fix of is_blank;
1998-03-10, by wenzelm
New scanner in abstract form.
1998-03-10, by nipkow
New simplifier flag for mutual simplification.
1998-03-10, by nipkow
Removed expand_split from simpset.
1998-03-10, by nipkow
removed pred;
1998-03-09, by wenzelm
eliminated pred function;
1998-03-09, by wenzelm
Symbol.explode;
1998-03-09, by wenzelm
replaced $LOGNAME by $USER;
1998-03-09, by wenzelm
tuned;
1998-03-09, by wenzelm
Symbol.is_*;
1998-03-09, by wenzelm
adapted to new scanner, baroque chars;
1998-03-09, by wenzelm
Symbol.input;
1998-03-09, by wenzelm
adapted to symbols, scan;
1998-03-09, by wenzelm
Generic scanners (for potentially infinite input) -- replaces Scanner;
1998-03-09, by wenzelm
adapted to new scanner and abroque chars;
1998-03-09, by wenzelm
read_var;
1998-03-09, by wenzelm
Symbol.output;
1998-03-09, by wenzelm
tuned syntax error msg;
1998-03-09, by wenzelm
Symbol.explode;
1998-03-09, by wenzelm
scan.ML, symbol.ML;
1998-03-09, by wenzelm
adapted to new scanners and baroque chars;
1998-03-09, by wenzelm
tuned some names;
1998-03-09, by wenzelm
adapted to baroque chars;
1998-03-09, by wenzelm
added merge_alists;
1998-03-09, by wenzelm
Syntax.indexname;
1998-03-09, by wenzelm
tuned comment;
1998-03-09, by wenzelm
tuned;
1998-03-09, by wenzelm
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
1998-03-09, by wenzelm
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
1998-03-09, by wenzelm
Removed `addsplits [expand_if]'
1998-03-07, by nipkow
added clasimp.ML;
1998-03-06, by wenzelm
Removed superfluous `op'
1998-03-06, by nipkow
*** empty log message ***
1998-03-06, by nipkow
Added delspilts, Addsplits, Delsplits.
1998-03-06, by nipkow
expand_if is now by default part of the simpset.
1998-03-06, by nipkow
New theorem and simprules
1998-03-05, by paulson
Reorganized simplifier. May now reorient rules.
1998-03-04, by nipkow
Reorganized simplifier. May now reorient rules.
1998-03-04, by nipkow
Reorganized simplifier. May now reorient rules.
1998-03-04, by nipkow
Better simplification allows deletion of parts of proofs
1998-03-03, by paulson
New theorem
1998-03-03, by paulson
New theorems
1998-03-03, by paulson
New theorems; tidied
1998-03-03, by paulson
New theorem diff_Suc_le_Suc_diff; tidied another proof
1998-03-03, by paulson
auto generated
1998-03-03, by paulson
Modified def.
1998-02-28, by nipkow
Splitters via named loopers.
1998-02-28, by nipkow
Little reorganization. Loop tactics have names now.
1998-02-28, by nipkow
Tried to reorganize rewriter a little. More to be done.
1998-02-28, by nipkow
added minimal description of rep_cs: corrections
1998-02-27, by oheimb
added minimal description of rep_cs
1998-02-27, by oheimb
added minimal description of rep_ss
1998-02-27, by oheimb
"choice" moved to Set.ML
1998-02-27, by paulson
New absorbsion laws, etc
1998-02-27, by paulson
Vimage
1998-02-27, by paulson
New vimage laws
1998-02-27, by paulson
added smart_tac
1998-02-26, by oheimb
removed superfluous addss
1998-02-26, by oheimb
New theory, Vimage
1998-02-26, by paulson
Proved choice and bchoice; changed Fun.thy -> thy
1998-02-26, by paulson
*** empty log message ***
1998-02-26, by wenzelm
added clasimp.ML;
1998-02-26, by wenzelm
renamed rep_claset to rep_cs
1998-02-25, by oheimb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
1998-02-25, by oheimb
changed wrapper mechanism of classical reasoner
1998-02-25, by oheimb
added split_all_tac to claset()
1998-02-25, by oheimb
changed wrapper mechanism of classical reasoner
1998-02-25, by oheimb
New theory of the inverse image of a function
1998-02-24, by paulson
Added some lemmas.
1998-02-24, by nipkow
Catches bad elim rules, handling exception OPTION
1998-02-23, by paulson
New laws for union
1998-02-23, by paulson
New laws for id
1998-02-23, by paulson
New induction schemas for lists (length and snoc).
1998-02-22, by nipkow
*** empty log message ***
1998-02-20, by nipkow
Congruence rules use == in premises now.
1998-02-20, by nipkow
Congruence rules use == in premises now.
1998-02-20, by nipkow
minor improvements
1998-02-20, by oheimb
re-arranged bindings for many function keys
1998-02-20, by oheimb
extended input syntax to handle names of special keys
1998-02-20, by oheimb
moved Ctrl entry before Alt entry
1998-02-20, by oheimb
New theorem eq_imp_le
1998-02-20, by paulson
Four new Union/Intersection laws
1998-02-19, by paulson
corrected problem with auto_tac: now uses a variant of depth_tac that avoids
1998-02-18, by oheimb
added New Jersey mirror;
1998-02-18, by wenzelm
Improved loop-test for rewrite rules a little.
1998-02-18, by nipkow
tuned comment;
1998-02-18, by wenzelm
added append (curried);
1998-02-13, by wenzelm
*** empty log message ***
1998-02-12, by wenzelm
Sign.merge vs. Sign.nontriv_merge;
1998-02-12, by wenzelm
tuned comments;
1998-02-12, by wenzelm
oops;
1998-02-12, by wenzelm
tuned print_cs;
1998-02-12, by wenzelm
updated;
1998-02-12, by wenzelm
tuned;
1998-02-12, by wenzelm
added explicit signature;
1998-02-12, by wenzelm
improved comments;
1998-02-12, by wenzelm
fixed add_trrules: intern root;
1998-02-12, by wenzelm
export map_trrule;
1998-02-12, by wenzelm
tuned add_trrules;
1998-02-12, by wenzelm
improved is_letter etc.;
1998-02-12, by wenzelm
New Addsimps for Compl rules
1998-02-10, by paulson
New AddIffs le_0_eq and neq0_conv
1998-02-10, by paulson
Replaced ALLNEWSUBGOALS by THEN_ALL_NEW
1998-02-09, by nipkow
Used THEN_ALL_NEW.
1998-02-09, by nipkow
moved freeze_thaw to drule.ML
1998-02-07, by paulson
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
1998-02-07, by paulson
AC and other rewrite rules for Un and Int
1998-02-07, by paulson
auto update
1998-02-07, by paulson
Added reference to rotate_prems
1998-02-07, by paulson
filter_size -> length_filter
1998-02-06, by nipkow
Added `remdups'
1998-02-06, by nipkow
added Vartab: TABLE;
1998-02-06, by wenzelm
added param;
1998-02-05, by wenzelm
added THEN_ALL_NEW;
1998-02-05, by wenzelm
New theorem Image_id
1998-02-05, by paulson
New theorem order_eq_refl
1998-02-05, by paulson
New max, min theorems
1998-02-05, by paulson
Added some more explicit guarantees of key secrecy for agents
1998-02-05, by paulson
Fixed a lot of overfull and underfull lines (hboxes)
1998-02-05, by paulson
Updated the description of how to set up hyp_subst_tac
1998-02-05, by paulson
New example, Pow_Sigma_bij
1998-02-02, by paulson
fixed WWW links
1998-02-02, by paulson
Three new facts about Image
1998-02-02, by paulson
Replaced \\1 by $1 as Perl itself asked me to...
1998-02-02, by paulson
Fixed the description of recdef
1998-01-30, by paulson
tuned msgs;
1998-01-30, by wenzelm
improved tracing of rewrite rule application;
1998-01-30, by wenzelm
removed dead messy code;
1998-01-30, by wenzelm
added read_var;
1998-01-30, by wenzelm
tuned;
1998-01-30, by wenzelm
Updated MOD reference
1998-01-23, by paulson
added symbols syntax;
1998-01-21, by wenzelm
reorganized into individual theories;
1998-01-20, by wenzelm
tuned;
1998-01-19, by wenzelm
make images;
1998-01-19, by wenzelm
tuned URL;
1998-01-15, by wenzelm
polyml-3.1;
1998-01-15, by wenzelm
obsolete;
1998-01-15, by wenzelm
added thms wrt weakening and strengthening in Abstraction;
1998-01-14, by mueller
New Jersey inactive;
Isabelle98
1998-01-14, by wenzelm
HOL/record;
1998-01-14, by wenzelm
error with instantiantion of sub-records removed
1998-01-14, by narasche
added record.ML;
1998-01-14, by wenzelm
tuned;
1998-01-14, by wenzelm
added unit and prod stuff;
1998-01-14, by wenzelm
fixed Id;
1998-01-14, by wenzelm
smlnj-110 factory default;
1998-01-14, by wenzelm
added of_sort;
1998-01-14, by wenzelm
added base_path;
1998-01-13, by wenzelm
added simulations files to IOA;
1998-01-13, by mueller
added forward simulation correectness;
1998-01-13, by mueller
Simplification: sel make and update make
1998-01-13, by narasche
added abstraction files;
1998-01-12, by mueller
added further IOA liles;
1998-01-12, by mueller
updated to Isabelle98;
1998-01-12, by wenzelm
tuned;
1998-01-12, by wenzelm
added files containing temproal logic and abstraction;
1998-01-12, by mueller
Delsimprocs nat_cancel;
1998-01-12, by wenzelm
tuned;
1998-01-12, by wenzelm
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
1998-01-12, by paulson
tuned;
1998-01-12, by wenzelm
tuned;
1998-01-12, by wenzelm
fixed author;
1998-01-12, by wenzelm
Simplified proofs by omitting PA = {|XA, ...|} from RA2
1998-01-10, by paulson
trivial tidy
1998-01-10, by paulson
tuned;
1998-01-09, by wenzelm
automatic index.html patch;
1998-01-09, by wenzelm
tuned;
1998-01-09, by wenzelm
tuned ISABELLE_TMP_PREFIX;
1998-01-09, by wenzelm
thm_ord;
1998-01-09, by wenzelm
eliminated make_ord;
1998-01-09, by wenzelm
ISABELLE_TMP_PREFIX: $LOGNAME
1998-01-09, by wenzelm
several minor updates;
1998-01-09, by wenzelm
tuned;
1998-01-08, by wenzelm
index.html for Isabelle Distribution Area;
1998-01-08, by wenzelm
updated to Isabelle98;
1998-01-08, by wenzelm
tuned;
1998-01-08, by wenzelm
fixed thm_less;
1998-01-08, by wenzelm
Expressed most Oops rules using Notes instead of Says, and other tidying
1998-01-08, by paulson
added split_paired_Ex to the implicit simpset
1998-01-08, by oheimb
added select_equality to the implicit claset
1998-01-08, by oheimb
added select_equality to the implicit claset
1998-01-08, by oheimb
added newline at end of file
1998-01-08, by oheimb
*** empty log message ***
1998-01-08, by oheimb
streamlined specification of included theories
1998-01-08, by oheimb
corrected Title
1998-01-08, by oheimb
removed obsolete comment
1998-01-08, by oheimb
added Univalent
1998-01-08, by oheimb
removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses
1998-01-08, by oheimb
added update_same, update_other, update_triv, and map_of_SomeD
1998-01-08, by oheimb
replaced fn _ => by K
1998-01-08, by oheimb
*** empty log message ***
1998-01-08, by wenzelm
New rule: image_subset
1998-01-08, by paulson
Restored the ciphertext in OR4 in order to make the spec closer to that in
1998-01-08, by paulson
Tidied by adding more default simprules
1998-01-08, by paulson
adapted to new split order;
1998-01-07, by wenzelm
adapted to new sort function;
1998-01-07, by wenzelm
improved targets;
1998-01-07, by wenzelm
tuned;
1998-01-06, by wenzelm
added -u option (again);
1998-01-05, by wenzelm
Now calls Blast_tac more often
1998-01-05, by paulson
obsolete;
1998-01-02, by wenzelm
feeder;
1998-01-02, by wenzelm
Changed required by new blast_tac (the one that squashes flex-flex pairs)
1998-01-02, by paulson
Blast_tac now squashes flex-flex pairs immediately
1998-01-02, by paulson
New theorem image_subsetI
1998-01-02, by paulson
Making proofs faster, especially using keysFor_parts_insert
1998-01-02, by paulson
do require perl;
1998-01-02, by wenzelm
Auto_tac now has type tactic, not unit->tactic
1998-01-02, by paulson
Declared startTiming and endTiming
1998-01-02, by paulson
use feeder to pipe into ML;
1997-12-31, by wenzelm
removed -i option;
1997-12-31, by wenzelm
nth -> !
1997-12-30, by nipkow
nth -> !
1997-12-30, by nipkow
feed isabelle session;
1997-12-29, by wenzelm
commented out symboloutput.pl;
1997-12-29, by wenzelm
added feeder.pl;
1997-12-29, by wenzelm
pretty_name_space;
1997-12-29, by wenzelm
removed declared;
1997-12-29, by wenzelm
removed distinct_fst_string;
1997-12-29, by wenzelm
improved error handling;
1997-12-28, by wenzelm
fixed execute;
1997-12-28, by wenzelm
made MLWorks happy;
1997-12-28, by wenzelm
stderr to $LOG;
1997-12-28, by wenzelm
Symtab.empty;
1997-12-28, by wenzelm
improved internal representation;
1997-12-28, by wenzelm
renamed Symtab.null to Symtab.empty;
1997-12-28, by wenzelm
renamed Symtab.null to Symtab.empty;
1997-12-28, by wenzelm
renamed Symtab.null to Symtab.empty;
1997-12-28, by wenzelm
added >> : (theory -> theory) -> unit;
1997-12-28, by wenzelm
tuned;
1997-12-28, by wenzelm
replaced symtab.ML by table.ML;
1997-12-28, by wenzelm
renamed (is_)null to (is_)empty;
1997-12-28, by wenzelm
Generic tables (lacking delete operation). Implemented as 2-3 trees.
1997-12-27, by wenzelm
tuned;
1997-12-24, by wenzelm
export range_type;
1997-12-24, by wenzelm
improved comment;
1997-12-24, by wenzelm
More restrictive patterns to prevent changing comments
1997-12-24, by paulson
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-24, by paulson
Tidied using rev_iffD1
1997-12-23, by paulson
Now Blast_tac works properly
1997-12-23, by paulson
Tidied. Also better proof using new blast_tac
1997-12-23, by paulson
Decremented subscript because of change to iffD1
1997-12-23, by paulson
Tidied using rev_iffD1, etc
1997-12-23, by paulson
Tidied using rev_iffD1
1997-12-23, by paulson
Tidied using more default rules
1997-12-23, by paulson
Overloading info for image
1997-12-23, by paulson
tidied
1997-12-23, by paulson
New rules rev_iffD{1,2}
1997-12-23, by paulson
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
1997-12-23, by paulson
New "obvious theorems"
1997-12-23, by paulson
Added range-type for completeness
1997-12-22, by paulson
New example
1997-12-22, by paulson
New rules rev_iffD{1,2}
1997-12-22, by paulson
corrected removal to /tmp/tmp.c
1997-12-19, by oheimb
added removal to /tmp/tmp.txt
1997-12-19, by oheimb
records without signature
1997-12-19, by narasche
remove signatrue from records
1997-12-19, by narasche
tuned;
1997-12-19, by wenzelm
new version;
1997-12-19, by wenzelm
added record.ML;
1997-12-19, by wenzelm
first version of records
1997-12-19, by narasche
pasted old insertion sort (does not work with new sort function!)
1997-12-19, by wenzelm
adapted to new sort function;
1997-12-19, by wenzelm
log file;
1997-12-19, by wenzelm
leading 0s;
1997-12-19, by wenzelm
tuned;
1997-12-19, by wenzelm
adapted to new sort function;
1997-12-19, by wenzelm
log files;
1997-12-19, by wenzelm
tuned;
1997-12-19, by wenzelm
added rev_order, make_ord;
1997-12-19, by wenzelm
term order;
1997-12-19, by wenzelm
term order stuff moved to term.ML;
1997-12-19, by wenzelm
log file;
1997-12-19, by wenzelm
'clean' target;
1997-12-19, by wenzelm
adapted to new sort function;
1997-12-19, by wenzelm
Term.termless;
1997-12-19, by wenzelm
adapted to new sort function;
1997-12-19, by wenzelm
removed maketest;
1997-12-19, by wenzelm
showtime - print time.
1997-12-18, by wenzelm
added expand_split_asm
1997-12-18, by oheimb
UNIV_I no longer counts as safe
1997-12-18, by paulson
tuned;
1997-12-17, by wenzelm
added mlworks;
1997-12-17, by wenzelm
added MLWorks;
1997-12-17, by wenzelm
misc improvements;
1997-12-17, by wenzelm
tuned tmp file name;
1997-12-17, by wenzelm
tuned comment;
1997-12-17, by wenzelm
added ML-Systems/mlworks.ML;
1997-12-17, by wenzelm
MLWorks startup script (for 1.0r2 or later).
1997-12-16, by wenzelm
renamed to mlworks.ML;
1997-12-16, by wenzelm
Compatibility file for MLWorks version 1.0r2 or later.
1997-12-16, by wenzelm
expandshort;
1997-12-16, by wenzelm
Simplified proofs using rewrites for f``A where f is injective
1997-12-16, by paulson
Simplified SpyKeys and ClientKeyExch as suggested by James Margetson
1997-12-16, by paulson
obsolete;
1997-12-16, by wenzelm
tuned;
1997-12-16, by wenzelm
obsolete;
1997-12-16, by wenzelm
adapted from Larry's version;
1997-12-16, by wenzelm
improved;
1997-12-16, by wenzelm
improved COMMIT_RO;
1997-12-15, by wenzelm
tuned;
1997-12-15, by wenzelm
polyml-3.1;
1997-12-15, by wenzelm
make smlnj-110 default;
1997-12-15, by wenzelm
tuned;
1997-12-15, by wenzelm
tuned;
1997-12-15, by wenzelm
No longer depend on theory context!
1997-12-15, by wenzelm
version = "Isabelle98: Jan 1998";
1997-12-13, by wenzelm
tuned comment;
1997-12-13, by wenzelm
smlnj-110;
1997-12-13, by wenzelm
deleted smlnj-1.09.ML;
1997-12-12, by wenzelm
obsolete;
1997-12-12, by wenzelm
Compatibility file for Standard ML of New Jersey.
1997-12-12, by wenzelm
tuned;
1997-12-12, by wenzelm
prepared for Isabelle98;
1997-12-12, by wenzelm
added;
1997-12-12, by wenzelm
obsolete;
1997-12-12, by wenzelm
tuned;
1997-12-12, by wenzelm
tuned msg;
1997-12-12, by wenzelm
tuned;
1997-12-12, by wenzelm
major update;
1997-12-12, by wenzelm
SYNC;
1997-12-12, by wenzelm
new blast_tac no longer works here
1997-12-12, by paulson
More deterministic (?) contr_tac
1997-12-12, by paulson
More deterministic and therefore faster (sometimes) proof reconstruction
1997-12-12, by paulson
ugly patch for new Blast_tac
1997-12-12, by paulson
Faster proof of mult_less_cancel2
1997-12-12, by paulson
tuned;
1997-12-11, by wenzelm
Tidied final proof
1997-12-11, by paulson
Tidied proof of finite_subset_induct
1997-12-11, by paulson
Got rid of mod2_neq_0
1997-12-11, by paulson
\subsection{*Theory inclusion};
1997-12-08, by wenzelm
Tidying to fix overfull lines, etc
1997-12-08, by paulson
Comprehensive (??) list of bugs, fixed or not
1997-12-08, by paulson
tuned;
1997-12-07, by wenzelm
added print_claset;
1997-12-07, by wenzelm
Replaced Fib(Suc n)~=0 by 0<Fib(Suc(n)).
1997-12-06, by nipkow
Got rid of some preds and replaced some n~=0 by 0<n.
1997-12-06, by nipkow
Cleaned up arithmetic mess.
1997-12-06, by nipkow
instantiate';
1997-12-05, by wenzelm
changed typed_print_translation;
1997-12-05, by wenzelm
tuned;
1997-12-05, by wenzelm
nat_cancel enabled by default;
1997-12-05, by wenzelm
adapted proofs to cope with simprocs nat_cancel;
1997-12-05, by wenzelm
improved arbitrary_def: we now really don't know nothing about it!
1997-12-05, by wenzelm
use_thy no longer requires writable current directory;
1997-12-05, by wenzelm
adapted proofs to cope with simprocs nat_cancel (by Stefan Berghofer);
1997-12-05, by wenzelm
simplification procedures nat_cancel enabled by default;
1997-12-05, by wenzelm
tmp_name;
1997-12-05, by wenzelm
added print_simpset;
1997-12-04, by wenzelm
added is_base;
1997-12-04, by wenzelm
added reset_context;
1997-12-04, by wenzelm
added eq_set;
1997-12-04, by wenzelm
moved global_names ref to Pure/ROOT.ML;
1997-12-04, by wenzelm
pred -> -1
1997-12-04, by nipkow
pred n -> n-1
1997-12-04, by nipkow
Simplified proofs.
1997-12-04, by nipkow
Added thm mult_div_cancel
1997-12-04, by nipkow
n ~= 0 should become 0 < n
1997-12-03, by nipkow
Replaced n ~= 0 by 0 < n
1997-12-03, by nipkow
pass return code!!
1997-12-03, by wenzelm
Fixed the treatment of substitution for equations, restricting occurrences of
1997-12-03, by paulson
updated for latest Blast_tac, which treats equality differently
1997-12-03, by paulson
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
1997-12-03, by paulson
Tidying and some comments
1997-12-03, by paulson
updated for latest Blast_tac, which treats equality differently
1997-12-03, by paulson
Instantiated the one-point-rule quantifier simpprocs for FOL
1997-12-03, by paulson
updated for latest Blast_tac, which fixes an equality bug
1997-12-03, by paulson
Miniscoping now used except for one proof
1997-12-03, by paulson
adapted to new term order;
1997-12-02, by wenzelm
tuned term order;
1997-12-02, by wenzelm
tuned trfuns types;
1997-12-02, by wenzelm
added prod_ord, dict_ord, list_ord;
1997-12-02, by wenzelm
File.tmp_name;
1997-12-02, by wenzelm
added tmp_name;
1997-12-02, by wenzelm
ISABELLE_TMP;
1997-12-02, by wenzelm
added context.ML;
1997-12-02, by wenzelm
Global contexts: session and theory.
1997-12-02, by wenzelm
added Thy/context.ML;
1997-12-02, by wenzelm
open;
1997-12-01, by wenzelm
nat_cancel simprocs;
1997-12-01, by wenzelm
ISABELLE_TMP_PREFIX;
1997-12-01, by wenzelm
ISABELLE_TMP;
1997-12-01, by wenzelm
Added DiffCancelSums.
1997-12-01, by berghofe
New guarantee B_trusts_NS5, and tidying
1997-12-01, by paulson
speed-up
1997-12-01, by paulson
args for record data
1997-12-01, by narasche
Removed "open Mutil;"
1997-11-28, by nipkow
Added comments
1997-11-28, by paulson
New timing functions startTiming and endTiming
1997-11-28, by paulson
addsplits now in FOL, ZF too
1997-11-28, by paulson
New example
1997-11-28, by paulson
Printing of statistics including time for search & reconstruction
1997-11-28, by paulson
New example
1997-11-28, by paulson
Removed dead code.
1997-11-28, by nipkow
Moved the quantifier elimination simp procs into Provers.
1997-11-28, by nipkow
Quantifier elimination procs.
1997-11-28, by nipkow
Fixed the definition of `termord': is now antisymmetric.
1997-11-28, by nipkow
several minor updates;
1997-11-27, by wenzelm
SYNC;
1997-11-27, by wenzelm
removed read_cterms;
1997-11-27, by wenzelm
fixed warning;
1997-11-27, by wenzelm
removed same_thm;
1997-11-27, by wenzelm
Tidying, mostly indentation
1997-11-27, by paulson
Deleted some needless addSIs; got rid of a slow Blast_tac
1997-11-27, by paulson
mk_norm_sum;
1997-11-27, by wenzelm
separate lists of simprocs;
1997-11-26, by wenzelm
Added rule impCE'
1997-11-26, by paulson
Blast_tac can prove Pelletier\'s problem 46\!
1997-11-26, by paulson
Tidying and using equalityCE instead of the slower equalityE
1997-11-26, by paulson
The change from iffE to iffCE means fewer case splits in most cases. Very few
1997-11-26, by paulson
Tidying
1997-11-26, by paulson
Tidying and modification to cope with iffCE
1997-11-26, by paulson
Added rule impCE'
1997-11-26, by paulson
Changes to AddIs improve performance of Blast_tac
1997-11-26, by paulson
Statistics
1997-11-26, by paulson
updated comment
1997-11-26, by paulson
Tidying and modification to cope with iffCE
1997-11-26, by paulson
added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;
1997-11-26, by wenzelm
added Arith provers;
1997-11-26, by wenzelm
Setup various arithmetic proof procedures.
1997-11-26, by wenzelm
added dest_nat;
1997-11-26, by wenzelm
moved to Arith/;
1997-11-26, by wenzelm
Cancel common constant factor from balanced exression.
1997-11-26, by wenzelm
Cancel common summands of balanced expressions.
1997-11-26, by wenzelm
removed conv_prover;
1997-11-26, by wenzelm
tuned;
1997-11-26, by wenzelm
added crep_cterm;
1997-11-26, by wenzelm
fixed type of thms_containing;
1997-11-26, by wenzelm
added foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a;
1997-11-26, by wenzelm
cleaned signature;
1997-11-26, by wenzelm
removed merge_opts;
1997-11-26, by wenzelm
managed merge details;
1997-11-25, by mueller
resolved merge conflict;
1997-11-25, by mueller
Added read_def_cterms for simultaneous reading/typing of terms under
1997-11-24, by nipkow
fixed warning;
1997-11-22, by wenzelm
made SML/NJ happy;
1997-11-22, by wenzelm
tuned;
1997-11-22, by wenzelm
replaced by seq.ML;
1997-11-21, by wenzelm
changed Pure/Sequence interface;
1997-11-21, by wenzelm
SYNC;
1997-11-21, by wenzelm
cd, use: path variables;
1997-11-21, by wenzelm
comment;
1997-11-21, by wenzelm
obsolete;
1997-11-21, by wenzelm
changed Pure/Sequence interface -- isatool fixseq;
1997-11-21, by wenzelm
changed Sequence interface (now Seq, in seq.ML);
1997-11-21, by wenzelm
cd, use etc. now support path variables;
1997-11-21, by wenzelm
fix references to obsolete Pure/Sequence structure;
1997-11-21, by wenzelm
tidying
1997-11-21, by paulson
analz_mono_contra_tac was wrong
1997-11-21, by paulson
Deleted some useless comments
1997-11-21, by paulson
minor improvements of formulation and proofs
1997-11-21, by oheimb
corrected INDUCT_FILES
1997-11-21, by oheimb
$ISABELLE_HOME/src;
1997-11-20, by wenzelm
improved error msg;
1997-11-20, by wenzelm
removed old note;
1997-11-20, by wenzelm
adapted print methods;
1997-11-20, by wenzelm
improved theorems print method: transfer_sg;
1997-11-20, by wenzelm
init_data: improved print method;
1997-11-20, by wenzelm
removed data.ML (made part of sign.ML);
1997-11-20, by wenzelm
added type object = exn;
1997-11-20, by wenzelm
added transfer_sg;
1997-11-20, by wenzelm
fixed xstr token encoding;
1997-11-20, by wenzelm
tuned infer_types interface;
1997-11-20, by wenzelm
tuned infer_types interface;
1997-11-20, by wenzelm
moved Sign.print_sg to display.ML;
1997-11-20, by wenzelm
exported pretty_classrel, pretty_arity;
1997-11-20, by wenzelm
added get_error: 'a error -> string option, get_ok: 'a error -> 'a option;
1997-11-20, by wenzelm
added implode_xstr: string list -> string, explode_xstr: string -> string list;
1997-11-20, by wenzelm
Now uses induct_tac
1997-11-20, by paulson
Updated the NatSum example
1997-11-20, by paulson
New, higher-level definition of \\out macro
1997-11-20, by paulson
Speeded up the proof of succ_lt_induct_lemma
1997-11-20, by paulson
Two new rewrites
1997-11-20, by paulson
Got rid of some slow deepen_tac calls
1997-11-20, by paulson
Renamed "overload" to "overloaded" for sml/nj compatibility
1997-11-20, by paulson
No more makeatletter/other
1997-11-20, by paulson
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
1997-11-18, by paulson
The dtac was discarding information, though apparently no proofs were hurt
1997-11-18, by paulson
Fixed bug in inst_split.
1997-11-18, by berghofe
improved big_rec_name lookup;
1997-11-17, by wenzelm
Updated comments. A bug causes MLWorks to use much
1997-11-17, by paulson
Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
1997-11-17, by paulson
Tuned function mk_cntxt_splitthm.
1997-11-17, by berghofe
Removed
1997-11-16, by nipkow
Redesigned the decision procedures for (Abelian) groups and commutative rings.
1997-11-15, by nipkow
Added
1997-11-15, by nipkow
merge_refs: check for different versions of theories;
1997-11-14, by wenzelm
export read_raw_typ;
1997-11-13, by wenzelm
fixed record parser;
1997-11-13, by wenzelm
improved record syntax;
1997-11-13, by wenzelm
made SML/NJ happy;
1997-11-13, by wenzelm
added thin_refl to hyp_subst_tac
1997-11-12, by oheimb
refer to $ISABELLE_HOME/src;
1997-11-12, by wenzelm
structure BasisLibrary;
1997-11-12, by wenzelm
renamed to use.ML;
1997-11-12, by wenzelm
Redefine 'use' command in order to support path variable expansion,
1997-11-12, by wenzelm
adapted to new Use, File structs;
1997-11-12, by wenzelm
added path variables;
1997-11-12, by wenzelm
File system operations.
1997-11-12, by wenzelm
moved old file stuff from library.ML to Thy/browser_info.ML;
1997-11-12, by wenzelm
added file.ML, use.ML;
1997-11-12, by wenzelm
tuned warning msg;
1997-11-12, by wenzelm
major cleanup;
1997-11-12, by wenzelm
moved 'latex' from library.ML to goals.ML;
1997-11-12, by wenzelm
tuned prths;
1997-11-12, by wenzelm
structure BasisLibrary;
1997-11-12, by wenzelm
added Thy/file.ML, Thy/use.ML;
1997-11-12, by wenzelm
renamed split_prem_tac to split_asm_tac
1997-11-12, by oheimb
restored last version
1997-11-12, by oheimb
simpdata.ML: renamed split_prem_tac to split_asm_tac, added split_if_asm
1997-11-12, by oheimb
renamed split_T_case_prem to split_T_case_asm
1997-11-12, by oheimb
renamed split_prem_tac to split_asm_tac
1997-11-12, by oheimb
renamed split_prem_tac to split_asm_tac
1997-11-12, by oheimb
Fixed indentation
1997-11-11, by paulson
Rationalized the theorem if_image_distrib.
1997-11-11, by paulson
Fixed indentation
1997-11-11, by paulson
Fixed spelling error
1997-11-11, by paulson
Made some proofs more robust
1997-11-11, by paulson
Now applies "map negOfGoal" to lits when expanding haz rules.
1997-11-11, by paulson
ASCII-fied;
1997-11-10, by wenzelm
polished definition of find_index_eq
1997-11-10, by oheimb
check files for non-ASCII characters;
1997-11-10, by wenzelm
replaced 8bit characters
1997-11-10, by oheimb
fixed LAM<...> syntax;
1997-11-10, by wenzelm
fixed spelling;
1997-11-10, by wenzelm
added split_prem_tac
1997-11-07, by oheimb
changed libraray function find to find_index_eq, currying it
1997-11-07, by oheimb
added contrapos
1997-11-07, by oheimb
added contrapos2
1997-11-07, by oheimb
added exists_Const
1997-11-07, by oheimb
Each datatype t now proves a theorem split_t_case_prem
1997-11-07, by nipkow
Perl no longer optional;
1997-11-06, by wenzelm
deriv: eliminated references to theory;
1997-11-06, by wenzelm
tuned;
1997-11-06, by wenzelm
tuned;
1997-11-06, by wenzelm
hyp_subst_tac checks if the equality has type variables and uses a suitable
1997-11-06, by paulson
subgoal_tac displays a warning if the new subgoal has type variables
1997-11-06, by paulson
mkdir -p bin;
1997-11-05, by wenzelm
Tools/8bit: ./mk;
1997-11-05, by wenzelm
*** empty log message ***
1997-11-05, by oheimb
tuned;
1997-11-05, by wenzelm
abandoned generation of tmp files
1997-11-05, by oheimb
various improvements
1997-11-05, by oheimb
reflecting changes of isa2latex
1997-11-05, by oheimb
several minor improvements
1997-11-05, by oheimb
added ax2isa
1997-11-05, by oheimb
added ax2isa
1997-11-05, by oheimb
added isabelle14 and isabelle24
1997-11-05, by oheimb
removed gererated files
1997-11-05, by oheimb
added entry for manual
1997-11-05, by oheimb
*** empty log message ***
1997-11-05, by oheimb
Now introduces Safe_tac
1997-11-05, by paulson
Ran expandshort, especially to introduce Safe_tac
1997-11-05, by paulson
Adapted to removal of UN1_I, etc
1997-11-05, by paulson
Adapted to removal of UN1_I, etc
1997-11-05, by paulson
UNIV now a constant; UNION1, INTER1 now translations and no longer have
1997-11-05, by paulson
Expandshort; new theorem le_square
1997-11-05, by paulson
generalized UNION1 to UNION
1997-11-05, by paulson
Tidied Key_supply3
1997-11-05, by paulson
fixed comment
1997-11-05, by paulson
UNIV & UNION1
1997-11-05, by paulson
Ran expandshort, especially to introduce Safe_tac
1997-11-05, by paulson
Ran expandshort, especially to introduce Safe_tac
1997-11-05, by paulson
adapted typed_print_translation;
1997-11-05, by wenzelm
tuned record_info;
1997-11-05, by wenzelm
fixed exception OPTION;
1997-11-05, by wenzelm
adapted pure_trfunsT;
1997-11-05, by wenzelm
print translation: added show_sorts argument;
1997-11-05, by wenzelm
adapted syn_ext_trfunsT;
1997-11-05, by wenzelm
adapted extend_trfunsT;
1997-11-05, by wenzelm
fixed exception OPTION;
1997-11-05, by wenzelm
added TYPE syntax;
1997-11-05, by wenzelm
fixed exception OPTION;
1997-11-05, by wenzelm
adapted add_trfunsT;
1997-11-05, by wenzelm
adapted add_trfunsT;
1997-11-05, by wenzelm
fixed exception OPTION;
1997-11-05, by wenzelm
base root = "";
1997-11-05, by wenzelm
Added an alternativ version of AutoChopper and a theory for the conversion of
1997-11-05, by nipkow
removed redundant ball_image
1997-11-04, by oheimb
removed redundant ball_empty and bex_empty (see equalities.ML)
1997-11-04, by oheimb
added several theorems
1997-11-04, by oheimb
added the, option_map, and case analysis theorems
1997-11-04, by oheimb
added zip and nodup
1997-11-04, by oheimb
added theorems for Eps
1997-11-04, by oheimb
tuned usage;
1997-11-04, by wenzelm
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
1997-11-04, by wenzelm
tuned to make non-Poly/MLs happy;
1997-11-04, by wenzelm
tuned 'records' stuff;
1997-11-04, by wenzelm
added pretty_ctyp;
1997-11-04, by wenzelm
tuned;
1997-11-04, by wenzelm
type object = exn (enhance readability);
1997-11-04, by wenzelm
*** empty log message ***
1997-11-04, by oheimb
* removed "axioms" and "generated by" section
1997-11-04, by oheimb
simplified (and corrected) syntax definition of fapp
1997-11-04, by oheimb
data kinds 'datatypes', data kinds 'records' added
1997-11-04, by narasche
removed old datatype_info;
1997-11-04, by wenzelm
added Thy/path.ML;
1997-11-04, by wenzelm
Logic.loops -> Logic.rewrite_rule_ok
1997-11-04, by nipkow
logic: loops -> rewrite_rule_ok
1997-11-04, by nipkow
added path.ML;
1997-11-04, by wenzelm
added base;
1997-11-04, by wenzelm
Abstract algebra of file paths. External representation Unix-style.
1997-11-04, by wenzelm
tuned;
1997-11-04, by wenzelm
removed old thy data stuff;
1997-11-04, by wenzelm
fixed set_current_thy pattern;
1997-11-04, by wenzelm
isatool fixclasimp;
1997-11-04, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
adapted to new datatypes thy info;
1997-11-03, by wenzelm
tuned;
1997-11-03, by wenzelm
datatypes;
1997-11-03, by wenzelm
nat datatype_info moved to Nat.thy;
1997-11-03, by wenzelm
added MLtext section;
1997-11-03, by wenzelm
added distinct_fst_string;
1997-11-03, by wenzelm
tuned: distinct_fst_string;
1997-11-03, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
export const_decls parser;
1997-11-03, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
CLASET';
1997-11-03, by wenzelm
moved cladata.ML, simpdata.ML to ROOT.ML;
1997-11-03, by wenzelm
adapted to new implicit claset;
1997-11-03, by wenzelm
adapted to new implicit simpset;
1997-11-03, by wenzelm
added claset thy_data;
1997-11-03, by wenzelm
added simpset thy_data;
1997-11-03, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
added thy_data;
1997-11-03, by wenzelm
use "hologic.ML"; use "cladata.ML"; use "simpdata.ML"; moved to ROOT.ML;
1997-11-03, by wenzelm
adapted to new implicit simpset;
1997-11-03, by wenzelm
adapted to new implicit claset;
1997-11-03, by wenzelm
fixed thy dependencies;
1997-11-03, by wenzelm
aded thy_data;
1997-11-03, by wenzelm
HOL theory data.
1997-11-03, by wenzelm
added thy_data.ML;
1997-11-03, by wenzelm
new implicit simpset mechanism based on Sign.sg anytype data;
1997-11-03, by wenzelm
new implicit claset mechanism based on Sign.sg anytype data;
1997-11-03, by wenzelm
adapted to new implicit claset mechanism;
1997-11-03, by wenzelm
fix references to implicit claset and simpset;
1997-11-03, by wenzelm
do not overwrite backup files;
1997-11-03, by wenzelm
set_session renamed to add_session;
1997-11-03, by wenzelm
tuned error msg;
1997-11-03, by wenzelm
made SML/97 happy;
1997-11-03, by wenzelm
expand_option_bind -> split_option_bind
1997-11-03, by nipkow
expand_option_case -> split_option_case
1997-11-03, by nipkow
*** empty log message ***
1997-11-03, by nipkow
expand_list_case -> split_list_case
1997-11-03, by nipkow
Indexed split_t_case.
1997-11-02, by nipkow
Documented `split_t_case' thm genearted by datatype.
1997-11-02, by nipkow
Fixed comments
1997-11-01, by paulson
New treatment of overloading\!
1997-11-01, by paulson
New syntax function for types
1997-11-01, by paulson
Faster lexing
1997-11-01, by paulson
New way of referring to Basis Library
1997-11-01, by paulson
mended type constraint\!
1997-11-01, by paulson
Set.thy was too specific
1997-11-01, by paulson
New Blast_tac (and minor tidying...)
1997-11-01, by paulson
Auto update
1997-11-01, by paulson
propagate exn msg;
1997-11-01, by wenzelm
dup sections: warning instead of error;
1997-10-31, by wenzelm
Session, Context;
1997-10-31, by wenzelm
tuned;
1997-10-31, by wenzelm
added mixfix_args;
1997-10-31, by wenzelm
*** empty log message ***
1997-10-31, by wenzelm
added str_of_sg: sg -> string;
1997-10-31, by wenzelm
added mixfix_args;
1997-10-30, by wenzelm
tuned thy_data;
1997-10-30, by wenzelm
tuned init_data;
1997-10-30, by wenzelm
added thy_data;
1997-10-30, by wenzelm
added merge_opts: ('a * 'a -> 'a) -> 'a option * 'a option -> 'a option;
1997-10-30, by wenzelm
Modified trace output routines of simplifier.
1997-10-30, by nipkow
domain package:
1997-10-30, by oheimb
domain package:
1997-10-30, by oheimb
domain package:
1997-10-30, by oheimb
domain package:
1997-10-30, by oheimb
PureThy.add_store_defs_i, PureThy.add_store_axioms;
1997-10-30, by wenzelm
fixed try_dest_adm;
1997-10-30, by wenzelm
added adm.ML;
1997-10-30, by wenzelm
tuned;
1997-10-30, by wenzelm
tuned simp trace;
1997-10-30, by wenzelm
*** empty log message ***
1997-10-30, by nipkow
Removed spurious blank.
1997-10-30, by nipkow
Updated proofs
1997-10-30, by nipkow
For each datatype `t' there is now a theorem `split_t_case' of the form
1997-10-30, by nipkow
fixed spaces in qed;
1997-10-29, by wenzelm
debugging concerning sort variables
1997-10-29, by oheimb
PureThy.add_store_axioms_i;
1997-10-28, by wenzelm
PureThy.add_store_defs_i, PureThy.add_store_axioms_i;
1997-10-28, by wenzelm
PureThy.add_store_defs_i;
1997-10-28, by wenzelm
PureThy.add_store_axioms;
1997-10-28, by wenzelm
fixed qed;
1997-10-28, by wenzelm
do not change global_names flag;
1997-10-28, by wenzelm
restructured -- uses PureThy storage facilities;
1997-10-28, by wenzelm
added ignored_consts, thms_containing, add_store_axioms(_i),
1997-10-28, by wenzelm
always reload .ML *and* .thy file;
1997-10-28, by wenzelm
PureThy.add_store_defs, PureThy.add_store_axioms;
1997-10-28, by wenzelm
added ancestors;
1997-10-28, by wenzelm
added name_of_thm;
1997-10-28, by wenzelm
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
1997-10-28, by wenzelm
eq_thm moved to thm.ML;
1997-10-28, by wenzelm
add_store_axioms_i;
1997-10-28, by wenzelm
Added finite_UNION/SigmaI.
1997-10-28, by nipkow
oops;
1997-10-27, by wenzelm
renamed put_* to store_*;
1997-10-27, by wenzelm
flipped global_names default;
1997-10-27, by wenzelm
do not change global_names flag;
1997-10-27, by wenzelm
Isa94-2 instead of Isa95;
1997-10-27, by wenzelm
adapted domain and ax_ops package for name spaces
1997-10-27, by oheimb
made SML/NJ happy;
1997-10-27, by wenzelm
Deleted two needless theorems
1997-10-27, by paulson
internalized some names
1997-10-25, by oheimb
corrected two comments
1997-10-25, by oheimb
Added
1997-10-24, by nipkow
oops, swap warnings;
1997-10-24, by wenzelm
record: tuned output;
1997-10-24, by wenzelm
ProtoPure.flexpair_def;
1997-10-24, by wenzelm
ProtoPure.flexpair_def;
1997-10-24, by wenzelm
merge: default to ProtoPure.thy;
1997-10-24, by wenzelm
ProtoPure.thy etc.;
1997-10-24, by wenzelm
tuned names;
1997-10-24, by wenzelm
self_ref: check_stale;
1997-10-24, by wenzelm
eq_thm (from drule.ML);
1997-10-24, by wenzelm
added declared: T -> string -> bool;
1997-10-24, by wenzelm
Pure.thy;
1997-10-24, by wenzelm
ProtoPure.thy;
1997-10-24, by wenzelm
tuned;
1997-10-24, by wenzelm
tuned;
1997-10-24, by wenzelm
removed add_thms_as_axms;
1997-10-24, by wenzelm
Init 'theorems' data. The Pure theories.
1997-10-24, by wenzelm
added pure_thy.ML;
1997-10-24, by wenzelm
tuned;
1997-10-24, by wenzelm
Modified comment.
1997-10-24, by nipkow
Deleted very odd Delsimps[Collect_False_empty] which made proofs fail!
1997-10-24, by nipkow
HOL/Map
1997-10-24, by nipkow
Added the new theory Map.
1997-10-24, by nipkow
added record section;
1997-10-23, by wenzelm
Sign.name_of;
1997-10-23, by wenzelm
Sign.stamp_names_of;
1997-10-23, by wenzelm
improved typ parser, exported;
1997-10-23, by wenzelm
tuned;
1997-10-23, by wenzelm
hide id, stamps;
1997-10-23, by wenzelm
Sign.stamp_names_of;
1997-10-23, by wenzelm
added sort_wrt;
1997-10-23, by wenzelm
fixed prune of hidden short names;
1997-10-23, by wenzelm
tuned;
1997-10-23, by wenzelm
tuned;
1997-10-22, by wenzelm
certify: check_stale;
1997-10-22, by wenzelm
improved handling of draft signatures / theories; draft thms (and
1997-10-21, by wenzelm
sg_ref: automatic adjustment of thms of draft theories;
1997-10-21, by wenzelm
commit;
1997-10-21, by wenzelm
made Poly/ML happy, but SML/NJ unhappy;
1997-10-21, by wenzelm
typo
1997-10-21, by nipkow
Corrected alphabetical order of entries in signature.
1997-10-21, by nipkow
Fixed the index entries for "recursion, general"
1997-10-21, by paulson
Many minor speedups:
1997-10-21, by paulson
New rewrite rules image_iff
1997-10-21, by paulson
Documented `addsplits'
1997-10-20, by nipkow
make SML/NJ happy;
1997-10-20, by wenzelm
rm IOA TLA;
1997-10-20, by wenzelm
tuned types;
1997-10-20, by wenzelm
tuned sig;
1997-10-20, by wenzelm
reset global_names;
1997-10-20, by wenzelm
set global_names;
1997-10-20, by wenzelm
replaced ops by consts;
1997-10-20, by wenzelm
removed Dlist;
1997-10-20, by wenzelm
\label{simp-chap} -> chap:simplification
1997-10-20, by nipkow
fixed goal_XXX;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
tuned;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
lookup long names of types;
1997-10-20, by wenzelm
tuned qualified names;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
qualified names;
1997-10-20, by wenzelm
local;
1997-10-20, by wenzelm
Sign.base_name;
1997-10-20, by wenzelm
fixed types of add_XXX;
1997-10-20, by wenzelm
fixed types of add_XXX;
1997-10-20, by wenzelm
tuned output;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
Sign.base_name;
1997-10-20, by wenzelm
fixed types of add_XXX;
1997-10-20, by wenzelm
local;
1997-10-20, by wenzelm
local section;
1997-10-20, by wenzelm
addsplits
1997-10-18, by nipkow
adapted to qualified names;
1997-10-17, by wenzelm
no longer tries bogus eta-contract involving aprops;
1997-10-17, by wenzelm
adapted to qualified names;
1997-10-17, by wenzelm
fixed RAW target;
1997-10-17, by wenzelm
(co) inductive / datatype package adapted to qualified names;
1997-10-17, by wenzelm
obselete 'end' hack;
1997-10-17, by wenzelm
global;
1997-10-17, by wenzelm
tuned "." syntax;
1997-10-17, by wenzelm
removed Classlib;
1997-10-17, by wenzelm
*** empty log message ***
1997-10-17, by wenzelm
setloop split_tac -> addsplits
1997-10-17, by nipkow
Added error messages.
1997-10-17, by nipkow
A lot of new comments
1997-10-17, by paulson
Eta-expanded a function decl to make sml/nj happy
1997-10-17, by paulson
Added "op" before "occs" to make sml/nj happy
1997-10-17, by paulson
New rewrite rules for simplifying conditionals
1997-10-17, by paulson
New trivial rewrites
1997-10-17, by paulson
New rewrite rules for simplifying conditionals
1997-10-17, by paulson
Better simplification eliminates a command from proof of psubset_card
1997-10-17, by paulson
New simprules imp_disj1,2 and some comments
1997-10-17, by paulson
Added image_eqI to simpset.
1997-10-17, by nipkow
Removed image_eqI from simpset because of clash with neq_shrK.
1997-10-17, by nipkow
AddIffs [all_not_in_conv];
1997-10-16, by nipkow
global;
1997-10-16, by wenzelm
Modified comment.
1997-10-16, by nipkow
New simprules imp_disj1, imp_disj2
1997-10-16, by paulson
New simprule diff_le_self, requiring a new proof of diff_diff_cancel
1997-10-16, by paulson
Removed comment.
1997-10-16, by nipkow
tuned;
1997-10-16, by wenzelm
removed begin;
1997-10-16, by wenzelm
fixed prep_ext;
1997-10-16, by wenzelm
Simplified proof.
1997-10-16, by nipkow
Simplified proof because of better simplifier.
1997-10-16, by nipkow
Various new lemmas. Improved conversion of equations to rewrite rules:
1997-10-16, by nipkow
added transfer: theory -> thm -> thm;
1997-10-16, by wenzelm
oops;
1997-10-16, by wenzelm
The simplifier has been improved a little: equations s=t which used to be
1997-10-16, by nipkow
fixed dependencies;
1997-10-16, by wenzelm
transfer thy Ord_nat;
1997-10-16, by wenzelm
sevaral goals restated in mono.thy;
1997-10-16, by wenzelm
moved rank_Inl, rank_Inr from Epsilon.ML to Univ.ML;
1997-10-16, by wenzelm
transfer InfDatatype.thy Limit_VfromE;
1997-10-16, by wenzelm
transfer CardinalArith.thy nat_into_Ord;
1997-10-16, by wenzelm
improved pretty_arity;
1997-10-16, by wenzelm
added merge_theories (new name arg);
1997-10-16, by wenzelm
fixed merge_theories;
1997-10-16, by wenzelm
revert to 1.3;
1997-10-16, by wenzelm
revert to 1.1;
1997-10-16, by wenzelm
Added last, butlast, dropped ttl.
1997-10-16, by nipkow
lala
1997-10-16, by mueller
Eta-expansion of function declarations, for value polymorphism
1997-10-16, by paulson
remove merge_theories;
1997-10-15, by wenzelm
make_draft replaced by prep_ext;
1997-10-15, by wenzelm
tuned;
1997-10-15, by wenzelm
eliminated aliasing merge: now always extends;
1997-10-15, by wenzelm
tuned comment;
1997-10-15, by wenzelm
improved print_data;
1997-10-15, by wenzelm
tuned;
1997-10-15, by wenzelm
slightly changed interfaces for oracles;
1997-10-15, by wenzelm
Added ack to Mateja Jamnik.
1997-10-15, by nipkow
tuned;
1997-10-15, by wenzelm
tuned;
1997-10-14, by wenzelm
added additional generic data;
1997-10-14, by wenzelm
Sign.print_data;
1997-10-14, by wenzelm
added init_data, get_data, put_data;
1997-10-14, by wenzelm
added data.ML;
1997-10-14, by wenzelm
Arbitrarily typed data.
1997-10-14, by wenzelm
Patch to avoid simplification of ~EX to ALL~
1997-10-14, by paulson
Two lemmas are already in List.
1997-10-14, by nipkow
More lemmas, esp. ~Bex and ~Ball conversions.
1997-10-14, by nipkow
Added neagtion rules for Ball and Bex.
1997-10-14, by nipkow
tuned;
1997-10-14, by wenzelm
browser info;
1997-10-14, by wenzelm
rearranged and added TLA
1997-10-14, by paulson
fixed extern;
1997-10-13, by wenzelm
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
1997-10-13, by wenzelm
uses Sign.str_of_sort;
1997-10-13, by wenzelm
fixed dots;
1997-10-13, by wenzelm
print_goals: optional output of const types (set show_consts);
1997-10-13, by wenzelm
merge: drops path elements;
1997-10-13, by wenzelm
Absolute URL's for documentation
1997-10-13, by merz
non-transparent logo;
1997-10-13, by wenzelm
fixed dots;
1997-10-13, by wenzelm
hierachically structured name spaces;
1997-10-13, by wenzelm
Changed logo.
1997-10-12, by berghofe
Added command for copying new logo.
1997-10-12, by berghofe
fixed dots;
1997-10-10, by wenzelm
fixed dots;
1997-10-10, by wenzelm
fixed fixed dots;
1997-10-10, by wenzelm
fixed dots;
1997-10-10, by wenzelm
fixed dots;
1997-10-10, by wenzelm
tuned;
1997-10-10, by wenzelm
fixed dots;
1997-10-10, by wenzelm
fixed dots;
1997-10-10, by wenzelm
fixed dots;
1997-10-10, by wenzelm
BAD_space_explode;
1997-10-10, by wenzelm
tuned;
1997-10-10, by wenzelm
fixed space_explode, old one retained as BAD_space_explode;
1997-10-10, by wenzelm
scan_longid moved to Syntax/lexicon.ML;
1997-10-10, by wenzelm
constify: qualified is const;
1997-10-10, by wenzelm
added longid syntax;
1997-10-10, by wenzelm
added longid;
1997-10-10, by wenzelm
decode: qualified is always const;
1997-10-10, by wenzelm
tuned;
1997-10-10, by wenzelm
\n at end;
1997-10-09, by wenzelm
ensure that dots in formulas are followed by non-idents;
1997-10-09, by wenzelm
*** empty log message ***
1997-10-09, by wenzelm
no longer handles consts "" -- use syntax instead;
1997-10-09, by wenzelm
removed open;
1997-10-09, by wenzelm
fixed infix syntax;
1997-10-09, by wenzelm
added TLA stuff;
1997-10-09, by wenzelm
fixed oracle;
1997-10-09, by wenzelm
removed declIffOracle;
1997-10-09, by wenzelm
changed preference order of prtab entries;
1997-10-09, by wenzelm
fixed infix syntax;
1997-10-09, by wenzelm
improved oracles: named, many per theory;
1997-10-09, by wenzelm
improved oracle: name;
1997-10-09, by wenzelm
fixed get_axiom, invoke_oracle;
1997-10-09, by wenzelm
print_theory: added oracles;
1997-10-09, by wenzelm
tuned exports;
1997-10-09, by wenzelm
fixed axiom names;
1997-10-09, by wenzelm
symbols syntax;
1997-10-08, by wenzelm
A formalization of TLA in HOL -- by Stephan Merz;
1997-10-08, by wenzelm
improved types of add_XXX funs (xtyp etc.);
1997-10-07, by wenzelm
improved types of add_XXX funs (xtyp etc.);
1997-10-07, by wenzelm
tuned decode;
1997-10-07, by wenzelm
tuned internal mapping table;
1997-10-07, by wenzelm
tuned;
1997-10-07, by wenzelm
tuned warning msg;
1997-10-07, by wenzelm
tuned;
1997-10-07, by wenzelm
The Isabelle Logo;
1997-10-07, by wenzelm
fixed 'begin';
1997-10-06, by wenzelm
optional begin keyword;
1997-10-06, by wenzelm
"->" made syntax;
1997-10-06, by wenzelm
eliminated raise_term;
1997-10-06, by wenzelm
eliminated raise_term, raise_typ;
1997-10-06, by wenzelm
add_arities_i;
1997-10-06, by wenzelm
TODO: handle internal / external names;
1997-10-06, by wenzelm
now supports qualified names (intern vs. extern) !!!
1997-10-06, by wenzelm
eliminated raise_term, raise_typ;
1997-10-06, by wenzelm
tuned read_cterms;
1997-10-06, by wenzelm
eliminated raise_term, raise_typ;
1997-10-06, by wenzelm
new internal forms: add_classes_i, add_classrel_i, add_defsort_i, add_arities_i
1997-10-06, by wenzelm
tuned;
1997-10-06, by wenzelm
now uses new Sign.pretty_sort;
1997-10-06, by wenzelm
eliminated raise_term, raise_typ;
1997-10-06, by wenzelm
now uses Syntax.simple_str_of_sort;
1997-10-06, by wenzelm
added simple_str_of_sort;
1997-10-06, by wenzelm
eliminated raise_term;
1997-10-06, by wenzelm
added 'path' section;
1997-10-06, by wenzelm
added pretty_sort;
1997-10-06, by wenzelm
fixed raw_term_sorts (again!);
1997-10-06, by wenzelm
eliminated raise_ast, raise_term, raise_typ;
1997-10-06, by wenzelm
added sort_to_ast;
1997-10-06, by wenzelm
eliminated raise_ast;
1997-10-06, by wenzelm
RAW target;
1997-10-06, by wenzelm
syntactic constants;
1997-10-06, by wenzelm
Routine tidying up
1997-10-03, by paulson
fully qualified names: Theory.add_XXX;
1997-10-02, by wenzelm
fully qualified name: Theory.set_oracle;
1997-10-01, by wenzelm
exported separator;
1997-10-01, by wenzelm
fully qualified names: Theory.add_XXX;
1997-10-01, by wenzelm
moved theory stuff (add_defs etc.) here from drule.ML;
1997-10-01, by wenzelm
moved theory stuff (add_defs etc.) to theory.ML;
1997-10-01, by wenzelm
fully qualified name: Theory.merge_thy_list;
1997-10-01, by wenzelm
fully qualified names: Theory.add_XXX;
1997-10-01, by wenzelm
added name_space.ML;
1997-10-01, by wenzelm
added split_last;
1997-10-01, by wenzelm
Hierarchically structured name spaces.
1997-10-01, by wenzelm
Strengthened the possibility property for resumption so that it could have
1997-10-01, by paulson
Fixed ServerResume to check for ServerHello instead of making a new NB
1997-10-01, by paulson
Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
1997-10-01, by paulson
Exchanged the M and SID fields of the FINISHED messages to simplify proofs
1997-10-01, by paulson
Auto update
1997-10-01, by paulson
SYNC
1997-09-30, by berghofe
Removed "browse.tex".
1997-09-30, by berghofe
Added section describing the theory browser.
1997-09-30, by berghofe
Updated usage information for tool "usedir".
1997-09-30, by berghofe
Theory browser stuff has been moved to "present.tex".
1997-09-30, by berghofe
obsolete;
1997-09-30, by wenzelm
ISABELLE_USEDIR_OPTIONS="-i true"
1997-09-30, by wenzelm
Changed html data directory and names of graph files.
1997-09-30, by berghofe
There is now one single option -i for generating theory browsing
1997-09-30, by berghofe
Modified some links.
1997-09-30, by berghofe
Client, Server certificates now sent using the separate Certificate rule,
1997-09-30, by paulson
tuned;
1997-09-29, by wenzelm
superficial;
1997-09-29, by wenzelm
obsolete;
1997-09-29, by wenzelm
margin 76 (2nd try :-);
1997-09-29, by wenzelm
fixed href to html library;
1997-09-29, by wenzelm
improved warning;
1997-09-29, by wenzelm
default margin 76 (to accomodate warning and error default output);
1997-09-29, by wenzelm
Step_tac -> Safe_tac
1997-09-29, by paulson
Much tidying including step_tac -> clarify_tac or safe_tac; sometimes
1997-09-29, by paulson
Step_tac -> Safe_tac
1997-09-29, by paulson
Much tidying including "qed" instead of result(), and even qed_spec_mp,
1997-09-29, by paulson
Previously loaded the WRONG THEORY, ignoring Confluence...
1997-09-29, by paulson
Now using qed_spec_mp
1997-09-29, by paulson
result() -> qed; Step_tac -> Safe_tac
1997-09-29, by paulson
Step_tac -> Safe_tac
1997-09-29, by paulson
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
1997-09-29, by paulson
Default simpset tactics now dereference "simpset"
1997-09-29, by paulson
Added Safe_tac; all other default claset tactics now dereference "claset"
1997-09-29, by paulson
fast_tac HOL_cs -> Fast_tac, etc.
1997-09-29, by paulson
result() -> qed
1997-09-29, by paulson
Step_tac -> Safe_tac
1997-09-29, by paulson
Tidied proof of r_comp_rtrancl_eq
1997-09-29, by paulson
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
1997-09-29, by paulson
Step_tac -> Safe_tac
1997-09-29, by paulson
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
1997-09-29, by paulson
Safe_tac; qed_spec_mp in FOL
1997-09-29, by paulson
Minor tidying to use Clarify_tac, etc.
1997-09-26, by paulson
eliminated rules;
1997-09-26, by wenzelm
Clarify_tac and some textual improvements
1997-09-25, by paulson
Clarify_tac; general reorganization
1997-09-25, by paulson
Deleted obsolete version of clarify_tac
1997-09-25, by paulson
Deleted the unused list_mk_disj
1997-09-25, by paulson
Deleted the unused gtake and recoded enumerate to use foldl
1997-09-25, by paulson
Deleted an obsolete step in TrustServerFinished
1997-09-25, by paulson
Deleted obsolete axioms inj_serverK and isSym_serverK
1997-09-25, by paulson
Tidied proofs, using Clarify_tac
1997-09-25, by paulson
Changed some proofs to use Clarify_tac
1997-09-25, by paulson
Prints warnings using the "warning" function instead of "writeln"
1997-09-25, by paulson
Generalized and exported biresolution_from_nets_tac to allow the declaration
1997-09-25, by paulson
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
1997-09-25, by paulson
sessionK now indexed by nat instead of bool.
1997-09-24, by paulson
Tidied some proofs using clarify_tac
1997-09-24, by paulson
clarify_tac and a new simprule
1997-09-24, by paulson
Names and saves the theorem parts_spies_subset_used
1997-09-24, by paulson
pure_trfuns: added constraint;
1997-09-24, by wenzelm
added handle_error: ('a -> 'b) -> 'a -> 'b error;
1997-09-23, by wenzelm
index.html obsolete;
1997-09-23, by wenzelm
Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;
1997-09-22, by wenzelm
acks;
1997-09-22, by wenzelm
added Cambridge fs;
1997-09-22, by wenzelm
fixed pttrn syntax;
1997-09-22, by wenzelm
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
1997-09-22, by wenzelm
tuned pattern syntax;
1997-09-22, by wenzelm
tuned lambda_ast_tr, idtyp_ast_tr' to accomodate fix of idt/idts
1997-09-22, by wenzelm
fixed idt/idts vs. pttrn/pttrns;
1997-09-22, by wenzelm
Added Cambridge font server
1997-09-22, by paulson
obsolete;
1997-09-22, by wenzelm
Simplified SpyKeys to use sessionK instead of clientK and serverK
1997-09-22, by paulson
First working version with Oops event for session keys
1997-09-19, by paulson
Full version of TLS including session resumption, but no Oops
1997-09-19, by paulson
Deleted the obsolete theorem analz_UN1_synth
1997-09-19, by paulson
Global change: lost->bad and sees Spy->spies
1997-09-18, by paulson
Deleted the redundant identifier Says_imp_sees_Spy'
1997-09-17, by paulson
New proof of respond_Spy_not_see_session_key
1997-09-17, by paulson
Removed the simprule imp_disjL from the analz_image_..._ss to boost speed
1997-09-17, by paulson
Fixed comments
1997-09-17, by paulson
Spy can see Notes of the compromised agents
1997-09-17, by paulson
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
1997-09-17, by paulson
Addition of SessionIDs to the Hello and Finished messages
1997-09-16, by paulson
Deleted the redundant simprule not_parts_not_analz
1997-09-16, by paulson
Deleted the redundant simprule not_parts_not_analz
1997-09-16, by paulson
Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
1997-09-16, by paulson
TLS now with a distinction between premaster secret and master secret
1997-09-16, by paulson
extended adm_tac;
1997-09-12, by mueller
replaced print_goals_ref hook by print_current_goals_fn and
1997-09-11, by wenzelm
removed print_goals_ref (which was broken anyway);
1997-09-11, by wenzelm
Split base cases from "msg" to "atomic" in order
1997-09-11, by paulson
Now uses the generic induct_tac
1997-09-11, by paulson
auto update
1997-09-11, by paulson
Added Larry's test for preventing a datatype shadowing a theory.
1997-09-10, by nipkow
Example from HOLCF paper.
1997-09-09, by nipkow
Loads HoareEx now.
1997-09-09, by nipkow
adm_tac extended
1997-09-09, by mueller
moved extended adm_tac to new place
1997-09-09, by mueller
added ".ML" extension in "use" command
1997-09-08, by paulson
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
1997-09-05, by paulson
set_of_list
1997-09-04, by paulson
Deleted an obsolete description of rewrite_cterm. The current version uses
1997-09-04, by paulson
some minor changes;
1997-09-03, by mueller
new extended adm tactic introduced;
1997-09-03, by mueller
Added True_implies_equals
1997-09-02, by nipkow
Added Larry's equal_intr_rule
1997-09-02, by nipkow
added case_prover
1997-09-02, by oheimb
Simplified the statement of A_trusts_NS2
1997-08-21, by paulson
Replacing impOfSubs analz_mono by analz_insertI should improve convergence
1997-08-21, by paulson
Renamed set_of_list to set, and relevant theorems too
1997-08-21, by paulson
Replaced Suc(Suc 0) by 2; it improves readability a little
1997-08-21, by paulson
Renamed theorems of the form set_of_list_XXX to set_XXX
1997-08-21, by paulson
Added select1_equality
1997-08-10, by nipkow
added append_file;
1997-08-08, by wenzelm
This file has moved to Distribution/lib/images.
1997-08-08, by berghofe
This file has moved to Distribution/lib/html.
1997-08-08, by berghofe
Removed references to simplifier.
1997-08-07, by berghofe
Modified parse error message.
1997-08-07, by berghofe
Startup script for Isabelle theory browser.
1997-08-07, by berghofe
Modified graph data directory.
1997-08-07, by berghofe
Added some commands for building theory browser.
1997-08-07, by berghofe
Added new environment variable ISABELLE_BROWSER_INFO.
1997-08-07, by berghofe
Added some code for generating theory browsing data.
1997-08-07, by berghofe
Gif images which are copied to $ISABELLE_BROWSER_INFO when
1997-08-07, by berghofe
Index file which is copied to $ISABELLE_BROWSER_INFO
1997-08-07, by berghofe
added str_of_classrel;
1997-08-06, by wenzelm
added "Proving ..." msgs;
1997-08-06, by wenzelm
renamed use_string to use_strings;
1997-08-06, by wenzelm
removed smlnj-1.07;
1997-08-06, by wenzelm
prs instead of TextIO.output;
1997-08-06, by wenzelm
tuned copy_file;
1997-08-06, by wenzelm
tuned names;
1997-08-06, by wenzelm
tuned;
1997-08-06, by wenzelm
ThmDatabase;
1997-08-06, by wenzelm
added read_file, write_file;
1997-08-06, by wenzelm
tuned;
1997-08-06, by wenzelm
use ThySyn.add_syntax;
1997-08-06, by wenzelm
tuned comments;
1997-08-06, by wenzelm
oops;
1997-08-06, by wenzelm
eliminated ThySynData and ThySynFun;
1997-08-06, by wenzelm
obsolete!
1997-08-06, by wenzelm
Replaced "init_thy_reader" by "set_parser".
1997-08-06, by berghofe
Removed references to "thy_data.ML".
1997-08-06, by berghofe
Moved some functions which used to be part of thy_data.ML
1997-08-06, by berghofe
Moved functions contained in this file to HOL.ML, datatype.ML,
1997-08-06, by berghofe
Replaced "init_thy_reader" by "set_parser".
1997-08-06, by berghofe
Removed reference to "thy_data.ML".
1997-08-06, by berghofe
The functions in this file have been moved to "cladata.ML"
1997-08-06, by berghofe
Moved functions from file "thy_data.ML".
1997-08-06, by berghofe
Replaced "init_thy_reader" by "set_parser".
1997-08-06, by berghofe
Replaced "init_thy_reader" by set_parser.
1997-08-06, by berghofe
Added some new dependencies for files in subdirectory Thy.
1997-08-06, by berghofe
Added function "file_exists".
1997-08-06, by berghofe
Removed function file_exists (now included in library.ML)
1997-08-06, by berghofe
Moved functions for theory information storage / retrieval
1997-08-06, by berghofe
This file now contains all functions for generating html
1997-08-06, by berghofe
Moved several functions:
1997-08-06, by berghofe
Moved "qed" - functions etc. from thy_read.ML to thm_database.ML.
1997-08-06, by berghofe
Added some additional "use" commands for new files
1997-08-06, by berghofe
Source files for Isabelle theory graph browser.
1997-08-06, by berghofe
Makefile for GraphBrowser
1997-08-06, by berghofe
added getenv;
1997-08-05, by wenzelm
removed smlnj-1.07;
1997-08-05, by wenzelm
cleaned up;
1997-08-05, by wenzelm
tuned comments;
1997-08-05, by wenzelm
removed ML-Systems/smlnj-1.07.ML;
1997-08-05, by wenzelm
SML/NJ 1.07 no longer supported!
1997-08-05, by wenzelm
cleaned up;
1997-08-05, by wenzelm
Added example mapf which requires a special congruence rule.
1997-08-05, by nipkow
Added function `replicate' and lemmas map_cong and set_replicate.
1997-08-05, by nipkow
cleaned up;
1997-08-05, by wenzelm
Corrected a comment
1997-08-05, by paulson
Added a take/dropWhile lemma.
1997-08-04, by nipkow
Generalized nth_drop (Conny).
1997-08-01, by nipkow
Corected bug in def of dropWhile (also present in Haskell lib!)
1997-08-01, by nipkow
Had to remove {x.x=a} = a from !simpset in one proof.
1997-08-01, by nipkow
Added {x.x=a} = a to !simpset.
1997-08-01, by nipkow
removed split_paired_Ex;
1997-07-25, by wenzelm
new simproc
1997-07-25, by nipkow
*** empty log message ***
1997-07-25, by wenzelm
load simplifier.ML (again);
1997-07-25, by wenzelm
added prems argument to simplification procedures;
1997-07-25, by wenzelm
remove references to simplifier.ML;
1997-07-25, by wenzelm
improved rewrite_thm / rewrite_goals to handle conditional eqns;
1997-07-25, by wenzelm
Added a few lemmas.
1997-07-24, by nipkow
Deleted comment.
1997-07-24, by nipkow
Replaced clumsy rewriting by the new function simplify on thms.
1997-07-24, by nipkow
List.ML: added lemmas by Stefan Merz.
1997-07-24, by nipkow
set_of_list -> set
1997-07-24, by paulson
Simplified a few proofs because of improved simplification.
1997-07-23, by nipkow
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
1997-07-23, by nipkow
added simplification meta rules;
1997-07-23, by wenzelm
standard congs;
1997-07-23, by wenzelm
Now rename_params_rule merely issues warnings--and does nothing--if the
1997-07-23, by paulson
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
1997-07-23, by paulson
Uses new version of Datatype.occs_in_prems
1997-07-23, by paulson
auto update
1997-07-23, by paulson
Removal of tactical STATE
1997-07-23, by paulson
fixed polymorphic val;
1997-07-23, by wenzelm
tuned congs: standard;
1997-07-23, by wenzelm
improved simp tracing;
1997-07-23, by wenzelm
added simplification meta rules;
1997-07-23, by wenzelm
tmp fix to accomodate rep_ss changes;
1997-07-23, by wenzelm
added rewrite_thm;
1997-07-23, by wenzelm
tuned apsome;
1997-07-23, by wenzelm
added error_msg;
1997-07-22, by wenzelm
tuned error / warning;
1997-07-22, by wenzelm
added print_ss;
1997-07-22, by wenzelm
added dest_mss, merge_mss;
1997-07-22, by wenzelm
tuned title;
1997-07-22, by wenzelm
added dest and merge operations;
1997-07-22, by wenzelm
added pretty_cterm;
1997-07-22, by wenzelm
improved print_cs;
1997-07-22, by wenzelm
Cosmetic changes: margins, indentation, ...
1997-07-22, by paulson
Now possibility_tac is an explicit function, in order to delay
1997-07-22, by paulson
Cosmetic changes: margins, indentation, ...
1997-07-22, by paulson
Now possibility_tac and basic_possibility_tac are explicit functions, in order
1997-07-22, by paulson
Deleted the superfluous assumption A ~= B, which must hold anyway by induction
1997-07-22, by paulson
Fixed the spelling of AUTH_NAMES--it could not have worked before\!
1997-07-22, by paulson
Option is a synonym for General because MLWorks does not yet provide
1997-07-22, by paulson
Removal of the tactical STATE
1997-07-22, by paulson
Removal of the tactical STATE
1997-07-22, by paulson
tuned error propagation msg;
1997-07-18, by wenzelm
defs may now be conditional;
1997-07-18, by wenzelm
renamed |-> <-| <-> to Parse/PrintRule;
1997-07-18, by wenzelm
tuned warning;
1997-07-18, by wenzelm
tuned warnings;
1997-07-18, by wenzelm
considered removal of print_goals_ref;
1997-07-18, by wenzelm
defs: allow conditions;
1997-07-18, by wenzelm
tuned warning;
1997-07-18, by wenzelm
renamed |-> <-| <-> to Parse/PrintRule;
1997-07-18, by wenzelm
tuned warning;
1997-07-18, by wenzelm
tuned warning;
1997-07-18, by wenzelm
improved output channels: normal, warning, error;
1997-07-18, by wenzelm
fixed EqI meta rule;
1997-07-17, by wenzelm
changes needed for introducing fairness
1997-07-17, by mueller
changes neede for introducing fairness
1997-07-17, by mueller
changes needed for adding fairness
1997-07-17, by mueller
fixed merge of internal simprocs;
1997-07-16, by wenzelm
Changing "lost" from a parameter of protocol definitions to a constant.
1997-07-14, by paulson
Fixed delIffs to deal correctly with the D-rule
1997-07-14, by paulson
Removed redundant addsimps of Un_insert_left, which is now a default simprule
1997-07-14, by paulson
Removal of monotonicity reasoning involving "lost" and the theorem
1997-07-11, by paulson
Now uses the Notes constructor to distinguish the Client (who has chosen M)
1997-07-11, by paulson
Moved some declarations to Message from Public and Shared
1997-07-11, by paulson
Now loads theory Event, which contains common declarations
1997-07-11, by paulson
Moving common declarations and proofs from theories "Shared"
1997-07-11, by paulson
removed obsolete init_pps and init_thy_reader;
1997-07-09, by wenzelm
improved type checking errors;
1997-07-09, by wenzelm
removed init_pps;
1997-07-09, by wenzelm
removed init_database;
1997-07-09, by wenzelm
Improved length = size translation.
1997-07-09, by nipkow
New proofs involving CERTIFICATE VERIFY
1997-07-07, by paulson
eliminated chmod -w;
1997-07-07, by wenzelm
-w option;
1997-07-07, by wenzelm
NOWRITE;
1997-07-07, by wenzelm
added -w option;
1997-07-07, by wenzelm
Changed some variables of type msg to lower case (e.g. from NB to nb
1997-07-04, by paulson
New constant "certificate"--just an abbreviation
1997-07-04, by paulson
Reduced priority of postfix ^* etc operators such that they are the same as
1997-07-04, by nipkow
Automatic update
1997-07-04, by paulson
Now catches the error of calling tgoalw when there are no goals to prove,
1997-07-04, by paulson
Simplified the new proofs about division
1997-07-04, by paulson
New comments on how to deal with unproved termination conditions
1997-07-04, by paulson
Fixed comments
1997-07-04, by paulson
Moved MLWorks.ML to its proper place, directory ML-Systems.
1997-07-04, by paulson
Automatic update
1997-07-04, by paulson
Modified the \tydx command to set types in italics instead of \tt
1997-07-03, by paulson
Some LaTeX-2e primitives such as \texttt
1997-07-03, by paulson
Added documentation for recdef, and tidied some other material
1997-07-03, by paulson
Updated references
1997-07-03, by paulson
set_of_list -> set
1997-07-03, by nipkow
Now there are TWO spaces after each full stop, so that the Emacs sentence
1997-07-02, by paulson
Now there are TWO spaces after each full stop, so that the Emacs sentence
1997-07-02, by paulson
Added the following lemmas tp Divides and a few others to Arith and NatDef:
1997-07-02, by nipkow
Tidying; also simplified the lemma Says_Server_not
1997-07-01, by paulson
New theory TLS
1997-07-01, by paulson
Deleted a redundant A~=B in rules that refer to a previous event
1997-07-01, by paulson
More realistic model: the Spy can compute clientK and serverK
1997-07-01, by paulson
Reordered rules in analz_image_freshK_ss to improve clarity
1997-07-01, by paulson
Removal of the obsolete newN function
1997-07-01, by paulson
New theorem priK_inj_eq, injectivity of priK
1997-07-01, by paulson
spy_analz_tac: Restored iffI to the list of rules used to break down
1997-07-01, by paulson
New theory TLS
1997-07-01, by paulson
Baby TLS. Proofs work, but model seems unrealistic
1997-07-01, by paulson
New and stronger lemmas; more default simp/cla rules
1997-07-01, by paulson
Deleted the obsolete operators newK, newN and nPair
1997-07-01, by paulson
Now the possibility proof calls the appropriate tactic
1997-07-01, by paulson
Added a comment
1997-07-01, by paulson
Now Collect_mem_eq is a default simprule (how could it have ever been omitted?
1997-07-01, by paulson
New laws for the "lists" operator
1997-07-01, by paulson
More concat lemmas.
1997-06-30, by nipkow
Corrected indentations and margins after the renaming of "set_of_list"
1997-06-27, by paulson
set_of_list -> set
1997-06-26, by nipkow
Trivial changes in connection with the Yahalom paper.
1997-06-26, by paulson
oops;
1997-06-26, by wenzelm
rearrange pages of ps file to be printed as booklet (duplex);
1997-06-26, by wenzelm
amdI -> admI2
1997-06-26, by nipkow
Tuned Franz's proofs.
1997-06-26, by nipkow
Removal of structure Context and its replacement by a theorem list of
1997-06-23, by paulson
Removal of COND_CONG, which is just if_cong RS eq_reflection
1997-06-23, by paulson
Ran expandshort
1997-06-23, by paulson
New "congs" keyword for recdef theory section
1997-06-23, by paulson
removed old Makefile;
1997-06-20, by wenzelm
removed;
1997-06-20, by wenzelm
removed old Makefile;
1997-06-20, by wenzelm
removed old Makefile and compat files;
1997-06-20, by wenzelm
Made proofs more concise by replacing calls to spy_analz_tac by uses of
1997-06-19, by paulson
Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
1997-06-19, by paulson
New comments; a tidied proof
1997-06-19, by paulson
Two new rewrite rules--NOT included by default\!
1997-06-19, by paulson
Defines KeyWithNonce, which is used to prove the secrecy of NB
1997-06-18, by paulson
Addition of not_imp (which pushes negation into implication) as a default
1997-06-18, by paulson
Corrected Title in header lines
1997-06-18, by paulson
Streamlined proofs of the secrecy of NB and added authentication of A and B
1997-06-18, by paulson
Removed Says_Crypt_lost and Says_Crypt_not_lost.
1997-06-18, by paulson
Removed Says_Crypt_lost and Says_Crypt_not_lost.
1997-06-18, by paulson
Adapted proofs to the removal of Says_Crypt_lost and Says_Crypt_not_lost
1997-06-18, by paulson
Deleted spurious reference to Spy_not_see_NB, which by chance was defined
1997-06-18, by paulson
converse -> ^-1
1997-06-17, by nipkow
Type constraint added to ensure that "length" refers to lists. Maybe should
1997-06-16, by paulson
Replacing the primrec definition of "length" by a translation to the built-in
1997-06-16, by paulson
Tuned wf_iff_no_infinite_down_chain proof, based on Konrads ideas.
1997-06-13, by nipkow
changed compatible definition;
1997-06-13, by mueller
added deadlock
1997-06-12, by mueller
added deadlock freedom, polished definitions and proofs
1997-06-12, by mueller
Strengthened and streamlined the Yahalom proofs
1997-06-09, by paulson
Useful new lemma
1997-06-09, by paulson
eliminated non-ASCII;
1997-06-06, by wenzelm
Added
1997-06-06, by nipkow
improved function 'nonreserved'
1997-06-06, by oheimb
Removed a few redundant additions of simprules or classical rules
1997-06-06, by paulson
The name bex_conj_distrib was WRONG
1997-06-06, by paulson
Better miniscoping for bounded quantifiers
1997-06-06, by paulson
Tidying and simplification of declarations
1997-06-06, by paulson
Much polishing of proofs
1997-06-06, by paulson
New miniscoping rules for ALL
1997-06-06, by paulson
New facts about In0/1 by Burkhart Wolff
1997-06-06, by paulson
New miniscoping rules ball_triv and bex_triv
1997-06-06, by paulson
Mended the definition of ack(0,n)
1997-06-06, by paulson
Two new examples; corrected a comment
1997-06-06, by paulson
New example theory: Recdef
1997-06-06, by paulson
added finite_converse
1997-06-05, by nipkow
Moved image_is_empty from Finite.ML to equalities.ML
1997-06-05, by nipkow
Modified a few defs and proofs because of the changes to theory Finite.thy.
1997-06-05, by nipkow
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
1997-06-05, by nipkow
New recdef examples
1997-06-05, by paulson
Removal of freeze_vars and thaw_vars. New freeze_thaw
1997-06-05, by paulson
freezeT now refers to Type.freeze_thaw
1997-06-05, by paulson
Tidying of signature. More robust renaming in freeze_thaw.
1997-06-05, by paulson
Removal of freeze_vars and thaw_vars (quite unused...)
1997-06-05, by paulson
Removal of radixstring from string_of_int; addition of string_of_indexname
1997-06-05, by paulson
There was never need for another copy of radixstring...
1997-06-05, by paulson
Numerous simplifications and removal of HOL-isms
1997-06-05, by paulson
Now loads theory Recdef
1997-06-05, by paulson
A slight simplification of optstring
1997-06-05, by paulson
Now extracts the predicate variable from induct0 insteead of trying to
1997-06-05, by paulson
Deleted the obsolete "pred_list" relation
1997-06-05, by paulson
Documented the new distinct_subgoals_tac
1997-06-05, by paulson
A slight simplification of optstring
1997-06-05, by paulson
Now extracts the predicate variable from induct0 insteead of trying to
1997-06-05, by paulson
Made the pseudo-type of split_rule_var a separate argument
1997-06-05, by paulson
eliminated non-ASCII;
1997-06-04, by wenzelm
eliminated freeze_vars;
1997-06-04, by wenzelm
changed priority of -> from [6,5]5 to [1,0]0
1997-06-04, by mueller
is_blank: fixed space2;
1997-06-03, by wenzelm
No longer refers to internal TFL structures
1997-06-03, by paulson
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
1997-06-03, by paulson
New theory "Power" of exponentiation (and binomial coefficients)
1997-06-03, by paulson
New theorem about the cardinality of the powerset (uses exponentiation)
1997-06-03, by paulson
Type inference makes a Const here, perhaps elsewhere?thry.sml
1997-06-02, by paulson
poly_tvars allows recdefs to be made without type constraints
1997-06-02, by paulson
Corrected banner: it is W0, not MiniML
1997-06-02, by paulson
New statement and proof of free_tv_subst_var in order to cope with new
1997-06-02, by paulson
Now Un_insert_left, Un_insert_right are default rewrite rules
1997-06-02, by paulson
Corrected statement of filter_append; added filter_size
1997-06-02, by paulson
Simplified proof
1997-06-02, by paulson
New theorems le_add_diff_inverse, le_add_diff_inverse2
1997-06-02, by paulson
trivial changes to incorporate CTL.thy and Example.ML in html file;
1997-05-30, by mueller
Simplified the calling sequence of CONTEXT_REWRITE_RULE
1997-05-30, by paulson
Moved "less_eq" to NatDef from Arith
1997-05-30, by paulson
New results including the basis for unique factorization
1997-05-30, by paulson
Now "primes" is a set
1997-05-30, by paulson
Now Divides must be the parent
1997-05-30, by paulson
New proofs about cardinality. Suggested by Florian Kammueller
1997-05-30, by paulson
Addition of Finite as parent allows cardinality theorems
1997-05-30, by paulson
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
1997-05-30, by paulson
Overloading of "^" requires a type constraint
1997-05-30, by paulson
Overloading of "^" requires new type class "power", with types "nat" and
1997-05-30, by paulson
New theory Divides
1997-05-30, by paulson
Many new theorems about cardinality
1997-05-30, by paulson
Now Divides must be the parent
1997-05-30, by paulson
Moving div and mod from Arith to Divides
1997-05-30, by paulson
flushOut ensures that no recent error message are lost (not certain this is
1997-05-30, by paulson
polyml-3.1 default again (for local work);
1997-05-27, by wenzelm
fixed -P (checkout only);
1997-05-27, by wenzelm
NJ 1.09.2x as factory default!
Isabelle94-8
1997-05-27, by wenzelm
Last changes for new release 94-8
1997-05-27, by mueller
added 1.09.28 note;
1997-05-27, by wenzelm
New theorems suggested by Florian Kammueller
1997-05-27, by paulson
Restoration of the two "bypassed" theorems Union_quotient and quotient_disj
1997-05-27, by paulson
Removal of card_insert_disjoint, which is now a default rewrite rule
1997-05-27, by paulson
New theorem disjoint_eq_subset_Compl
1997-05-27, by paulson
New theorem le_Suc_eq
1997-05-27, by paulson
Removal of mask.sig and mask.sml
1997-05-27, by paulson
Removal of module Mask and datatype binding with its constructor |->
1997-05-27, by paulson
New theorems suggested by Florian Kammueller
1997-05-27, by paulson
remoded ccc1
1997-05-26, by slotosch
removed ccc1
1997-05-26, by slotosch
tuned comment;
1997-05-26, by wenzelm
Two useful facts about Powersets suggested by Florian Kammueller
1997-05-26, by paulson
Added a missing "result();" after problem 43.
1997-05-26, by paulson
Tidying using the new exhaust_tac
1997-05-26, by paulson
Now recdef checks the name of the function being defined.
1997-05-26, by paulson
Deleted option_case_tac because exhaust_tac performs a similar function.
1997-05-26, by paulson
Renamed lessD to Suc_leI
1997-05-26, by paulson
New operator "lists" for formalizing sets of lists
1997-05-26, by paulson
New theorem subset_inj_onto
1997-05-26, by paulson
Two results suggested by Florian Kammueller
1997-05-26, by paulson
Tidying and a couple of useful lemmas
1997-05-26, by paulson
Added recdef
1997-05-26, by paulson
Primrec: New example ported from ZF
1997-05-26, by paulson
Renamed lessD to Suc_leI
1997-05-26, by paulson
New example ported from ZF
1997-05-26, by paulson
Simplified proofs using expand_option_case
1997-05-26, by paulson
Now checks the name of the function being defined;
1997-05-26, by paulson
More de-HOL-ification
1997-05-26, by paulson
Now checks the name of the function being defined
1997-05-26, by paulson
Deleted unused functions
1997-05-26, by paulson
Now a Perl script. No longer requires commands to be at the beginnings of
1997-05-26, by paulson
Slight simplifications
1997-05-26, by paulson
Eliminated ccc1. Moved ID,oo into Cfun.
1997-05-25, by slotosch
Moved the classes flat chfin from Fix to Pcpo.
1997-05-25, by slotosch
*** empty log message ***
1997-05-25, by slotosch
Eliminated the prediates flat,chfin
1997-05-25, by slotosch
eliminated the constant less by the introduction of the axclass sq_ord
1997-05-25, by slotosch
tuned;
1997-05-23, by wenzelm
arbitrary
1997-05-23, by nipkow
Added `arbitrary'
1997-05-23, by nipkow
fixed;
1997-05-23, by wenzelm
new syntactic priority of lambda abstraction
1997-05-23, by oheimb
adapted entry for addss, addSss
1997-05-23, by oheimb
news.
1997-05-23, by nipkow
Documented `size' function for datatypes.
1997-05-23, by nipkow
fixed a bug
1997-05-23, by mueller
removed TFL from test;
1997-05-23, by wenzelm
remove cl.cam font server;
1997-05-23, by wenzelm
exec the emacs;
1997-05-23, by wenzelm
Base theory is now Arith, not Nat. (because all datatypes now require Arith).
1997-05-23, by nipkow
All datatypes now require Arith.
1997-05-23, by nipkow
Added overloaded function `size' for all datatypes.
1997-05-23, by nipkow
exhaust_tac can now deal with whole terms rather than just variables.
1997-05-22, by nipkow
added href to Isamode;
1997-05-22, by wenzelm
fixed doc;
1997-05-22, by wenzelm
adapted to Isamode 2.6;
1997-05-22, by wenzelm
tuned Isamode stuff;
1997-05-22, by wenzelm
New headers and other minor changes
1997-05-22, by paulson
Now the recdef induction rule variables are named u, v, ...
1997-05-22, by paulson
New example of recdef and permutative rewriting
1997-05-22, by paulson
Now uses type option instead of Fail/Subst
1997-05-22, by paulson
Now uses type option instead of Fail/Subst
1997-05-22, by paulson
Uses option_case_tac
1997-05-22, by paulson
Deleted rprod: lex_prod is (usually?) enough
1997-05-22, by paulson
Deleted obsolete proofs. But option_case_tac will be obsolete too
1997-05-22, by paulson
New example: ex/Fib
1997-05-22, by paulson
New lemmas used for ex/Fib
1997-05-22, by paulson
Added rotation to exhaust_tac.
1997-05-22, by nipkow
tuned;
1997-05-22, by wenzelm
added;
1997-05-22, by wenzelm
tuned;
1997-05-22, by wenzelm
SYNC;
1997-05-22, by wenzelm
Documented exhaust_tac.
1997-05-22, by nipkow
fixed packages;
1997-05-22, by wenzelm
fixed packages;
1997-05-22, by wenzelm
tuned comments;
1997-05-22, by wenzelm
Replaced res_inst-list_cases by generic exhaust_tac.
1997-05-22, by nipkow
Added exhaustion thm and exhaust_tac for each datatype.
1997-05-22, by nipkow
fixed find cmd;
1997-05-21, by wenzelm
set version;
1997-05-21, by wenzelm
tuned all READMEs;
1997-05-21, by wenzelm
release version (sort of);
1997-05-21, by wenzelm
SYNC;
1997-05-21, by wenzelm
fixed spelling;
1997-05-21, by wenzelm
changes for release 94-8
1997-05-21, by mueller
tuned;
1997-05-21, by wenzelm
Code tidying: removal of C combinator
1997-05-21, by paulson
Basis library input/output primitives; \!simpset instead of HOL_ss
1997-05-21, by paulson
Basis library input/output primitives; currying the induction rule;
1997-05-21, by paulson
TFL induction rule is now curried
1997-05-21, by paulson
Function "sum" now defined using primrec
1997-05-21, by paulson
Mostly cosmetic changes: updated headers, ID lines, etc.
1997-05-21, by paulson
Removed rprod from the WF relation
1997-05-21, by paulson
Removed rprod from the WF relation; simplified proofs;
1997-05-21, by paulson
Replaced Konrad's own add_term_names by the predefined one.
1997-05-21, by nipkow
tuned command line;
1997-05-20, by wenzelm
tuned;
1997-05-20, by wenzelm
under construction;
1997-05-20, by wenzelm
SYNC;
1997-05-20, by wenzelm
fix spelling;
1997-05-20, by wenzelm
the new README;
1997-05-20, by wenzelm
now generated automatically from README.html;
1997-05-20, by wenzelm
README generation;
1997-05-20, by wenzelm
removed Cambridge font server;
1997-05-20, by wenzelm
fixed bash path;
1997-05-20, by wenzelm
reset make_html afterwards;
1997-05-20, by wenzelm
fixed spelling;
1997-05-20, by wenzelm
IMPORTANT NOTE: This is the old README.
1997-05-20, by wenzelm
X11 font server sample configuration;
1997-05-20, by wenzelm
deleted duplicate rewrite rules of lift.simps
1997-05-20, by mueller
minor changes
1997-05-20, by mueller
tuned;
1997-05-20, by wenzelm
added eindhoven http address
1997-05-20, by mueller
Declares Option_ as synonym for structure Option
1997-05-20, by paulson
Removal of redundant code (unused or already present in Isabelle.
1997-05-20, by paulson
Basis library version of type "option" now resides in its own structure Option
1997-05-20, by paulson
Removal of ex/LexProd
1997-05-20, by paulson
Renamed egcd and gcd; defined the gcd function using TFL
1997-05-20, by paulson
Removal of duplicate code from TFL
1997-05-20, by paulson
New arithmetic laws let us delete three lines of a proof
1997-05-20, by paulson
Added comment: it is SLOW
1997-05-20, by paulson
Some theorems moved to HOL/Arith.ML
1997-05-20, by paulson
Relation "less_than" internalizes "<" for easy use of TFL
1997-05-20, by paulson
New pattern-matching definition of pred_nat
1997-05-20, by paulson
The diff laws must be named: we do "Delsimps [diff_Suc];"
1997-05-20, by paulson
New theorems from Hoare/Arith2.ML
1997-05-20, by paulson
new treatment of Prover files
1997-05-20, by paulson
Removal of ex/LexProd; TFL files; new treatment of Prover files
1997-05-20, by paulson
Removal of ex/LexProd
1997-05-20, by paulson
improved output syntax of op =, op ~= (more parentheses);
1997-05-20, by wenzelm
SYNC;
1997-05-20, by wenzelm
index: model checkers;
1997-05-20, by wenzelm
*** empty log message ***
1997-05-20, by wenzelm
SYNC;
1997-05-20, by wenzelm
little changes
1997-05-20, by mueller
Documented auto_tac
1997-05-19, by paulson
Section numbers may now be nested three deep, as in 1.2.3
1997-05-19, by paulson
Distributed Psubset stuff to basic set theory files, incl Finite.
1997-05-16, by nipkow
renamed unsafe_addss to addss
1997-05-16, by oheimb
readme added
1997-05-16, by mueller
commented out qed (in case the MC is unavailable);
1997-05-16, by mueller
added Modelcheck example;
1997-05-16, by mueller
still under construction!
1997-05-16, by wenzelm
improved www4 ref;
1997-05-16, by wenzelm
fixed infix syntax;
1997-05-16, by wenzelm
fixed Modelchek reference;
1997-05-16, by wenzelm
SYNC;
1997-05-16, by wenzelm
hint at more sections;
1997-05-16, by wenzelm
added \settdx;
1997-05-16, by wenzelm
Invoking Model Checkers in Isabelle/HOL;
1997-05-16, by mueller
renamed unsafe_addss to addss
1997-05-16, by oheimb
Subst now moved to directory HOL
1997-05-16, by paulson
renamed unsafe_addss to addss
1997-05-15, by oheimb
renamed addss to addSss, unsafe_addss to addss, extended auto_tac
1997-05-15, by oheimb
*** empty log message ***
1997-05-15, by wenzelm
corrected depth_tac: no call for safe_step_tac if subgoal not present
1997-05-15, by oheimb
fixed bash path!!!
1997-05-15, by wenzelm
SYNC;
1997-05-15, by wenzelm
removed garbage;
1997-05-15, by wenzelm
sysman refs;
1997-05-15, by wenzelm
remove FIXME;
1997-05-15, by wenzelm
New proofs for TFL
1997-05-15, by paulson
Improved error message in "require_thy"
1997-05-15, by paulson
Added pred_list for TFL
1997-05-15, by paulson
Preliminary TFL versions
1997-05-15, by paulson
TFL theory section
1997-05-15, by paulson
New theories used by TFL
1997-05-15, by paulson
New version, modified by Konrad Slind and LCP for TFL
1997-05-15, by paulson
TFL now integrated with HOL (more work needed)
1997-05-15, by paulson
remove Witness.thy;
1997-05-15, by wenzelm
SYNC;
1997-05-14, by wenzelm
preliminary!
1997-05-14, by wenzelm
added \tooldx;
1997-05-14, by wenzelm
tuned comment;
1997-05-14, by wenzelm
tuned;
1997-05-14, by wenzelm
renamed DEFAULT_LOGIC to ISABELLE_LOGIC;
1997-05-14, by wenzelm
removed -u option;
1997-05-14, by wenzelm
ML_SYSTEM is polyml-3.1 again;
1997-05-14, by wenzelm
tuned;
1997-05-14, by wenzelm
mylist instead of list in datatype ex;
1997-05-14, by wenzelm
tuned comment;
1997-05-14, by wenzelm
tuned;
1997-05-14, by wenzelm
tuned comments;
1997-05-14, by wenzelm
corrected problem with type abbreviations in pcpo_type
1997-05-13, by oheimb
of_sort: type_sig -> typ * sort -> bool;
1997-05-13, by wenzelm
added system, ind_defs, axclass;
1997-05-12, by wenzelm
fixed ISABELLE_DOCS multiple components;
1997-05-12, by wenzelm
*** empty log message ***
1997-05-12, by wenzelm
added System;
1997-05-12, by wenzelm
The Isabelle System Manual;
1997-05-12, by wenzelm
improved doc stuff;
1997-05-12, by wenzelm
added AxClass;
1997-05-12, by wenzelm
Tutorial on Axiomatic Type Classes;
1997-05-12, by wenzelm
list of manuals to be made automatically;
1997-05-12, by wenzelm
'dist', 'clean';
1997-05-12, by wenzelm
added 'clean';
1997-05-12, by wenzelm
move to Inductive/
1997-05-12, by wenzelm
moved here from ..
1997-05-12, by wenzelm
minor tuning;
1997-05-12, by wenzelm
minor tuning;
1997-05-12, by wenzelm
SYNC;
1997-05-12, by wenzelm
improved comments;
1997-05-12, by wenzelm
removed README;
1997-05-12, by wenzelm
partially adapted to axclass / instance;
1997-05-12, by wenzelm
obsolete;
1997-05-12, by wenzelm
removed Witness;
1997-05-12, by wenzelm
fixed dependecy: CPure;
1997-05-12, by wenzelm
misc tuning, cleanup, improvements;
1997-05-09, by wenzelm
minor tuning;
1997-05-09, by wenzelm
SYNC;
1997-05-09, by wenzelm
minor tuning;
1997-05-09, by wenzelm
tuned ref to src;
1997-05-09, by wenzelm
New theorems about "assign"
1997-05-09, by paulson
Fixed precedence of semicolon
1997-05-09, by paulson
New equivalence proofs
1997-05-09, by paulson
New proofs about WHILE and VALOF
1997-05-08, by paulson
Modified def of Least, which, as Markus correctly complained, looked like
1997-05-08, by nipkow
Made a slow proof slightly faster
1997-05-08, by paulson
Changed from fast_tac to blast_tac
1997-05-08, by paulson
misc minor improvements;
1997-05-07, by wenzelm
tuned;
1997-05-07, by wenzelm
replaced Int by IntPr, result by qed;
1997-05-07, by wenzelm
fixed ref to srcs;
1997-05-07, by wenzelm
fixed caption font;
1997-05-07, by wenzelm
tuned spaces;
1997-05-07, by wenzelm
fixed braces;
1997-05-07, by wenzelm
stylistic improvements
1997-05-07, by paulson
Documents directory Induct; stylistic improvements
1997-05-07, by paulson
New acknowledgements
1997-05-07, by paulson
fixed witness syntax;
1997-05-07, by wenzelm
SYNC;
1997-05-07, by wenzelm
New acknowledgements; fixed overfull lines and tables
1997-05-07, by paulson
New acknowledgements; no Fast_tac
1997-05-07, by paulson
Larry's private LaTeX-2e version
1997-05-07, by paulson
Moved induction examples to directory Induct
1997-05-07, by paulson
changed title to README
1997-05-07, by paulson
Documentation for directory "ex"
1997-05-07, by paulson
Documentation for directory "Induct"
1997-05-07, by paulson
Conversion to use blast_tac (with other improvements)
1997-05-07, by paulson
New directory to contain examples of (co)inductive definitions
1997-05-07, by paulson
Description of the Auth directory: security protocols proofs
1997-05-07, by paulson
fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);
1997-05-06, by wenzelm
tuned;
1997-05-06, by wenzelm
*** empty log message ***
1997-05-06, by wenzelm
tuned comments;
1997-05-06, by wenzelm
fixed simplifier ex;
1997-05-06, by wenzelm
SYNC;
1997-05-06, by wenzelm
fixed simplifier examples;
1997-05-06, by wenzelm
Stupid bug in induct_tac caused warning to always appear.
1997-05-06, by nipkow
removed MLtrans, MLtext;
1997-05-06, by wenzelm
added \Pure, \CPure;
1997-05-06, by wenzelm
misc updates, tuning, cleanup;
1997-05-06, by wenzelm
tuned;
1997-05-05, by wenzelm
tuned;
1997-05-05, by wenzelm
Cosmetic update of induct_tac; test first now.
1997-05-05, by nipkow
SYNC;
1997-05-05, by wenzelm
misc updates, tuning, cleanup;
1997-05-05, by wenzelm
less
more
|
(0)
-1920
+1920
+10000
+30000
tip