Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
more robust handling of theory context;
1999-02-05, by wenzelm
improved theory, context, update_context;
1999-02-05, by wenzelm
improved 'theory';
1999-02-05, by wenzelm
improved msg;
1999-02-05, by wenzelm
use_thy, update_thy: Context.save;
1999-02-05, by wenzelm
tuned;
1999-02-05, by wenzelm
time_use made pervasive;
1999-02-05, by wenzelm
use_dir: check parent, more robust exit;
1999-02-05, by wenzelm
more robust RC;
1999-02-05, by wenzelm
setmp: theory option;
1999-02-05, by wenzelm
Session.finish ();
1999-02-05, by wenzelm
tidied Schroeder-Bernstein proof
1999-02-05, by paulson
new surj rules
1999-02-05, by paulson
obsolete;
1999-02-04, by wenzelm
tuned;
1999-02-04, by wenzelm
include full paths in file info;
1999-02-04, by wenzelm
Symbol.use;
1999-02-04, by wenzelm
Symbol.use (eliminated Use.exit_use);
1999-02-04, by wenzelm
leave theory context after load_thy;
1999-02-04, by wenzelm
File.pwd, File.cd;
1999-02-04, by wenzelm
fixed file_info;
1999-02-04, by wenzelm
use, cd;
1999-02-04, by wenzelm
added 'use';
1999-02-04, by wenzelm
fail_safe close;
1999-02-04, by wenzelm
check_elem: allow ~, except for '~' and '~~';
1999-02-04, by wenzelm
removed use.ML;
1999-02-04, by wenzelm
removed General/use.ML;
1999-02-04, by wenzelm
made SML/NJ happy;
1999-02-03, by wenzelm
check_thy: include ML stamp;
1999-02-03, by wenzelm
added join_info;
1999-02-03, by wenzelm
tidied load path handling;
1999-02-03, by wenzelm
add_path / reset_path;
1999-02-03, by wenzelm
tuned;
1999-02-03, by wenzelm
ThmDatabase.ml_store_thm;
1999-02-03, by wenzelm
usedir -r;
1999-02-03, by wenzelm
Session.init;
1999-02-03, by wenzelm
Theory loader database: theory and file dependencies, theory values
1999-02-03, by wenzelm
tidied;
1999-02-03, by wenzelm
Session management -- maintain state of logic images.
1999-02-03, by wenzelm
get_lexicon;
1999-02-03, by wenzelm
tokenize: get exploded args;
1999-02-03, by wenzelm
delete_tmpfiles (from thy_read.ML);
1999-02-03, by wenzelm
added reset_path;
1999-02-03, by wenzelm
open BasicThmDatabase;
1999-02-03, by wenzelm
Theory presentation (fake implementation);
1999-02-03, by wenzelm
moved to Pure/context.ML;
1999-02-03, by wenzelm
nuked;
1999-02-03, by wenzelm
moved to General/use.ML;
1999-02-03, by wenzelm
removed load;
1999-02-03, by wenzelm
ThyInfo.begin_theory;
1999-02-03, by wenzelm
oops, update_thy;
1999-02-03, by wenzelm
removed load;
1999-02-03, by wenzelm
removed load;
1999-02-03, by wenzelm
comment;
1999-02-03, by wenzelm
removed load;
1999-02-03, by wenzelm
proper setup of preloaded theories (ThyInfo.register_theory);
1999-02-03, by wenzelm
renamed sig to PRIVATE_SIGN;
1999-02-03, by wenzelm
added thm, thms, Open_locale, Close_locale, Print_scope;
1999-02-03, by wenzelm
added Goal(w) and Export (from context.ML);
1999-02-03, by wenzelm
added is_draft;
1999-02-03, by wenzelm
enabled sig;
1999-02-03, by wenzelm
tuned msg;
1999-02-03, by wenzelm
Global theory context (used to be in Thy/context.ML);
1999-02-03, by wenzelm
moved several files;
1999-02-03, by wenzelm
more abstract implementation;
1999-02-03, by wenzelm
use Path.T;
1999-02-03, by wenzelm
of_file: Path.T, Position.T;
1999-02-03, by wenzelm
added use.ML;
1999-02-03, by wenzelm
added Use;
1999-02-03, by wenzelm
tuned;
1999-02-03, by wenzelm
tidied; added thy_load.ML
1999-02-03, by paulson
tidied, with left_inverse & right_inverse as default simprules
1999-02-03, by paulson
auto update
1999-02-03, by paulson
inj
1999-02-03, by paulson
documented typecheck_tac, etc
1999-02-03, by paulson
standard spelling: type-checking
1999-02-03, by paulson
inj is now a translation of inj_on
1999-02-03, by paulson
standard spelling: type-checking
1999-02-03, by paulson
a bit of tidying
1999-02-01, by paulson
Theory loader primitives.
1999-01-30, by wenzelm
corrected output of symbols for several (probably not all) relevant functions
1999-01-29, by oheimb
renamed space2 to spacespace
1999-01-29, by oheimb
corrected output of symbols for several (probably not all) relevant functions
1999-01-29, by oheimb
moved print_mode to ROOT.ML
1999-01-29, by oheimb
expandshort
1999-01-29, by paulson
expandshort
1999-01-29, by paulson
tidied
1999-01-29, by paulson
tidied
1999-01-28, by paulson
constdefs
1999-01-28, by paulson
tidying
1999-01-28, by paulson
arith_tac for min/max
1999-01-27, by nipkow
*** empty log message ***
1999-01-27, by wenzelm
ZF typechecking
1999-01-27, by paulson
automatic insertion of datatype intr rules into claset
1999-01-27, by paulson
new typechecking solver for the simplifier
1999-01-27, by paulson
tuned;
1999-01-25, by wenzelm
Fixed a bug in lin.arith.
1999-01-24, by nipkow
tuned;
1999-01-22, by wenzelm
tuned;
1999-01-22, by wenzelm
isabelle.in.tum.de;
1999-01-20, by wenzelm
http://isabelle.in.tum.de/dist/;
1999-01-20, by wenzelm
renamed variables for clarity
1999-01-20, by paulson
changed Minho mirror;
1999-01-20, by wenzelm
tidied freeness reasoning
1999-01-19, by paulson
freeness reasoning: T.free_iffs
1999-01-19, by paulson
tuned;
1999-01-19, by wenzelm
removal of the (thm list) argument of mk_cases
1999-01-19, by paulson
tidied; added dest_eq
1999-01-19, by paulson
simplified thanks to the arithmetic prover
1999-01-19, by paulson
updated comments
1999-01-19, by paulson
a simplification by G Bella
1999-01-19, by paulson
structure Graph = Graph;
1999-01-18, by wenzelm
GraphFun (generic directed graphs);
1999-01-18, by wenzelm
added General/graph.ML: generic direct graphs;
1999-01-18, by wenzelm
removed empty line (in case of empty begin_state marker) before Level line
1999-01-15, by oheimb
Removed superfluous arith rules from metric_simps
1999-01-14, by nipkow
More Arith.
1999-01-14, by nipkow
Fixed old bug: selection of constant to be split should depend not just on
1999-01-14, by nipkow
nat_arith_tac -> arith_tac
1999-01-14, by nipkow
More arith refinements.
1999-01-14, by nipkow
tuned README;
1999-01-14, by wenzelm
Pure/General/symbol.ML;
1999-01-14, by wenzelm
tuned;
1999-01-14, by wenzelm
deleted the appendices because documentation exists in the HOL and ZF manuals
1999-01-13, by paulson
defined dquotesoff
1999-01-13, by paulson
new manual ZF
1999-01-13, by paulson
the separate FOL and ZF logics manual, with new material on datatypes and
1999-01-13, by paulson
removal of FOL and ZF
1999-01-13, by paulson
minor updates on inductive definitions and datatypes
1999-01-13, by paulson
fixed titles;
1999-01-13, by wenzelm
tidying of datatype and inductive definitions
1999-01-13, by paulson
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
1999-01-13, by wenzelm
Refined arithmetic.
1999-01-13, by nipkow
congruence rules finally use == instead of = and <->
1999-01-13, by paulson
generalized qed_spec_mp code to work for ZF
1999-01-13, by paulson
datatype package improvements
1999-01-13, by paulson
better qed_spec_mp
1999-01-13, by paulson
Simplified interface.
1999-01-13, by nipkow
Simplified arithmetic.
1999-01-13, by nipkow
'same' method, 'immediate' proof;
1999-01-12, by wenzelm
tuned msg;
1999-01-12, by wenzelm
SYNC;
1999-01-12, by wenzelm
fixed again;
1999-01-12, by wenzelm
improved asm_finish;
1999-01-12, by wenzelm
get_tthms witness theorems;
1999-01-12, by wenzelm
Split argument structure.
1999-01-12, by nipkow
Restructured Arithmatic
1999-01-12, by nipkow
*** empty log message ***
1999-01-12, by nipkow
verbatim
1999-01-12, by nipkow
SYNC;
1999-01-12, by wenzelm
fixed deriv;
1999-01-12, by wenzelm
eliminated tthm type and Attribute structure;
1999-01-12, by wenzelm
tuned msg;
1999-01-12, by wenzelm
tuned signature;
1999-01-12, by wenzelm
eliminated global/local names;
1999-01-12, by wenzelm
eliminated tthm type and Attribute structure;
1999-01-12, by wenzelm
eliminated tthm type and Attribute structure;
1999-01-12, by wenzelm
eliminated Attribute structure;
1999-01-12, by wenzelm
signature BASIC_THM;
1999-01-12, by wenzelm
fixed AUTO_PERL;
1999-01-12, by wenzelm
show_tags;
1999-01-12, by wenzelm
added rule_attribute: ('a -> thm -> thm) -> 'a attribute;
1999-01-12, by wenzelm
Thm of string * tag list;
1999-01-12, by wenzelm
eliminated Attribute structure;
1999-01-12, by wenzelm
removed attribute.ML;
1999-01-12, by wenzelm
configure AUTO_BASH, AUTO_PERL;
1999-01-12, by wenzelm
Some simplifications.
1999-01-11, by nipkow
More arith simplifications
1999-01-11, by nipkow
More arith simplifications.
1999-01-11, by nipkow
more robust heap file detection;
1999-01-11, by wenzelm
tuned, updated;
1999-01-11, by wenzelm
tidying, e.g. from \\tt to \\texttt
1999-01-11, by paulson
Remoaved a few now redundant rewrite rules.
1999-01-09, by nipkow
Added simproc.
1999-01-09, by nipkow
Refined arith tactic.
1999-01-09, by nipkow
removal of FOL, ZF to a separate manual
1999-01-08, by paulson
removal of DO_GOAL
1999-01-08, by paulson
ZF: the natural numbers as a datatype
1999-01-07, by paulson
if-then-else syntax for ZF
1999-01-07, by paulson
if-then-else syntax for ZF
1999-01-07, by paulson
fixed commit spec;
1999-01-06, by wenzelm
Simplified proof.
1999-01-06, by nipkow
induct_tac and exhaust_tac
1999-01-06, by paulson
primrec, induct_tac
1999-01-06, by paulson
*** empty log message ***
1999-01-05, by nipkow
Small mods.
1999-01-05, by nipkow
1 proof now automatic.
1999-01-05, by nipkow
Instantiated lin.arith.
1999-01-05, by nipkow
In Main: moved Bin to the left to preserve the solver in its simpset.
1999-01-05, by nipkow
Shortened a proof.
1999-01-04, by nipkow
*** empty log message ***
1999-01-04, by nipkow
Version 1 of linear arithmetic for nat.
1999-01-04, by nipkow
Version 1.0 of linear nat arithmetic.
1999-01-04, by nipkow
added new arg for print_tac
1998-12-28, by paulson
new inductive, datatype and primrec packages, etc.
1998-12-28, by paulson
revised datatype definition package
1998-12-28, by paulson
revised inductive definition package
1998-12-28, by paulson
new primrec package
1998-12-28, by paulson
moved from ZF to new subdirectory Tools
1998-12-28, by paulson
new theorem update_type
1998-12-28, by paulson
converted to use new primrec section and update operator
1998-12-28, by paulson
converted to use new primrec section
1998-12-28, by paulson
fixed comment
1998-12-28, by paulson
Needs separate theory Primrec_defs due to new inductive defs package
1998-12-28, by paulson
more efficient strip_quotes using "substring"
1998-12-28, by paulson
Basis Library compatible substring oeration
1998-12-28, by paulson
Added a "message" argument to print_tac
1998-12-28, by paulson
comments
1998-12-28, by paulson
deleted "escape" and "trim"; Basis Library can do string escapes if necessary
1998-12-28, by paulson
String added to BasisLibrary
1998-12-28, by paulson
better indentation
1998-12-28, by paulson
fixed comments
1998-12-28, by paulson
replaced obsolete "trim" by "strip_quotes"
1998-12-28, by paulson
Link to HOLCF paper added.
1998-12-18, by nipkow
moved dest_Type to term.ML from HOL/Tools/primrec_package
1998-12-18, by paulson
moved dest_eq to hologic.ML and tidied
1998-12-18, by paulson
new function dest_eq
1998-12-18, by paulson
tuned mode_name;
1998-12-17, by wenzelm
bash -c :;
1998-12-17, by wenzelm
*** empty log message ***
1998-12-11, by oheimb
added new print_mode "xsymbols" for extended symbol support
1998-12-11, by oheimb
better representation of Sigma
1998-12-11, by oheimb
initisaterm now obsolete
1998-12-11, by oheimb
new Close_locale synatx
1998-12-11, by paulson
deleted unclosed comment
1998-12-11, by paulson
the + facility for locales, by Florian
1998-12-11, by paulson
new Close_locale synatx
1998-12-11, by paulson
towards handling sharing of variables
1998-12-07, by paulson
tidying
1998-12-07, by paulson
expandshort
1998-12-07, by paulson
better export for nested locales
1998-12-04, by paulson
new (and generalized) theorems about Sigma/Times
1998-12-04, by paulson
locales: assumes and defines may be empty
1998-12-04, by paulson
locales
1998-12-04, by paulson
and_list;
1998-12-03, by wenzelm
Addition of the States component; parts of Comp not working
1998-12-03, by paulson
tuned;
1998-12-02, by wenzelm
IOA-Storage: Memory storage case study.
1998-12-02, by wenzelm
Memory storage case study.
1998-12-02, by wenzelm
Memory storage case study from PhD p.240;
1998-12-02, by mueller
new theorem Pow_UNIV
1998-12-02, by paulson
new rule rev_bexI
1998-12-02, by paulson
new theorems Domain_Union, Range_Union
1998-12-02, by paulson
removed duplicate contrapos;
1998-12-01, by wenzelm
enum: !!! after seperator;
1998-12-01, by wenzelm
excursion: ERROR_MESSAGE;
1998-12-01, by wenzelm
qed: kind_name (again);
1998-12-01, by wenzelm
show_tags flag;
1998-12-01, by wenzelm
new theorem INT_Un
1998-12-01, by paulson
better version of Image_diag
1998-12-01, by paulson
tactical CHANGED now uses alpha-eta conversion, not alpha conversion
1998-11-30, by paulson
Renamed subset_Sigma_llist to subset_Times_llist
1998-11-30, by paulson
new theorems about diag
1998-11-30, by paulson
fixed declatation of patterns and skolem;
1998-11-29, by wenzelm
tuned print_state;
1998-11-29, by wenzelm
tuned welcome msg;
1998-11-29, by wenzelm
added restart;
1998-11-29, by wenzelm
added exception RESTART;
1998-11-29, by wenzelm
proof_general_trans (experimental);
1998-11-29, by wenzelm
replaced wakeup by decorate_prompt_fn;
1998-11-29, by wenzelm
eliminated "Trying to recover ..." msg;
1998-11-29, by wenzelm
added oct_char;
1998-11-29, by wenzelm
method brute_force = ALLGOALS force_tac;
1998-11-29, by wenzelm
*** empty log message ***
1998-11-27, by nipkow
At last: linear arithmetic for nat!
1998-11-27, by nipkow
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
1998-11-27, by nipkow
fixed a link
1998-11-27, by paulson
added Real/Hyperreal
1998-11-27, by paulson
Addition of Hyperreal theories Zorn and Filter
1998-11-27, by paulson
moved diag (diagonal relation) from Univ to Relation
1998-11-27, by paulson
tidied up list definitions, using type 'a option instead of
1998-11-26, by paulson
tuning to assimiliate it with PhD;
1998-11-26, by mueller
Added a general refutation tactic which works by putting things into nnf first.
1998-11-26, by nipkow
Added filter_prems_tac
1998-11-26, by nipkow
removed prs / prs_fn;
1998-11-25, by wenzelm
guarantees laws
1998-11-25, by paulson
simplified ensures_UNIV
1998-11-25, by paulson
new thms for invariant
1998-11-25, by paulson
new theorem program_equalityE
1998-11-25, by paulson
renamed vars
1998-11-25, by paulson
image_id in simpset
1998-11-25, by paulson
removed prs / prs_fn (broken, because it did not include \n in its
1998-11-25, by wenzelm
eliminated ISABELLE_INTERFACE_OPTIONS;
1998-11-25, by wenzelm
improved comment;
1998-11-25, by wenzelm
replaced prs by std_output;
1998-11-25, by wenzelm
replaced prs by writeln;
1998-11-25, by wenzelm
replaced prs by std_output / writeln;
1998-11-25, by wenzelm
comment parser;
1998-11-25, by wenzelm
add_text, add_chapter etc.: dummy;
1998-11-25, by wenzelm
chapter etc. headings;
1998-11-25, by wenzelm
tuned space;
1998-11-25, by wenzelm
replaced prs by writeln;
1998-11-25, by wenzelm
removed redirect_to_latex stuff;
1998-11-25, by wenzelm
Isar.main();
1998-11-24, by wenzelm
setup Blast.setup;
1998-11-24, by wenzelm
added commands;
1998-11-24, by wenzelm
added isar.ML;
1998-11-24, by wenzelm
Isabelle/Isar main interface.
1998-11-24, by wenzelm
fixed prefix_lines: *separate* by \n;
1998-11-24, by wenzelm
added Isar/isar.ML;
1998-11-24, by wenzelm
fixed links
1998-11-23, by paulson
print_state hook, obeys Goals.current_goals_markers by default;
1998-11-21, by wenzelm
print_state: use begin_goal from Goals.current_goals_markers;
1998-11-21, by wenzelm
added undos, redos;
1998-11-21, by wenzelm
tty: issue wakeup;
1998-11-21, by wenzelm
std_output, prefix_lines;
1998-11-21, by wenzelm
better miniscoping rules: the premise C~={} is not good
1998-11-20, by paulson
fixed method syntax;
1998-11-19, by wenzelm
break: exhibit state stack;
1998-11-19, by wenzelm
match_bind: 'as' patterns;
1998-11-19, by wenzelm
let: 'as' patterns;
1998-11-19, by wenzelm
match_bind(_i): 'as' patterns;
1998-11-19, by wenzelm
term_pat vs. prop_pat;
1998-11-19, by wenzelm
term_pat vs. prop_pat;
1998-11-19, by wenzelm
no warning for "it" theorems;
1998-11-19, by wenzelm
tidied
1998-11-18, by paulson
Finally removing "Compl" from HOL
1998-11-18, by paulson
exn_message FAIL;
1998-11-18, by wenzelm
blast: cla_method';
1998-11-18, by wenzelm
export simp_modifiers;
1998-11-18, by wenzelm
expoer cla_method('), cla_modifiers;
1998-11-18, by wenzelm
method setup;
1998-11-18, by wenzelm
tuned comments;
1998-11-18, by wenzelm
'prop', 'term', 'typ';
1998-11-18, by wenzelm
load;
1998-11-18, by wenzelm
export exn_message;
1998-11-18, by wenzelm
removed trace;
1998-11-18, by wenzelm
BREAK: include state;
1998-11-17, by wenzelm
have_tthms;
1998-11-17, by wenzelm
PureThy.default_name;
1998-11-17, by wenzelm
generalized (opt_)thm_name;
1998-11-17, by wenzelm
exception METHOD_FAIL;
1998-11-17, by wenzelm
added have_theorems, have_lemmas, have_facts;
1998-11-17, by wenzelm
added 'theorems', 'lemmas', 'note';
1998-11-17, by wenzelm
break: exhibit state;
1998-11-17, by wenzelm
exception ATTRIB_FAIL;
1998-11-17, by wenzelm
removed trace;
1998-11-17, by wenzelm
Symbol.space;
1998-11-17, by wenzelm
space;
1998-11-17, by wenzelm
val spc: int -> T;
1998-11-17, by wenzelm
added default_name;
1998-11-17, by wenzelm
Drule.rev_triv_goal;
1998-11-17, by wenzelm
Theory.apply replaced by Library.apply;
1998-11-17, by wenzelm
val apply: ('a -> 'a) list -> 'a -> 'a;
1998-11-17, by wenzelm
export vars_of and friends;
1998-11-17, by wenzelm
Pretty.spc;
1998-11-17, by wenzelm
added pretty_tthms, print_tthms;
1998-11-17, by wenzelm
new theory UNITY/PPROD
1998-11-17, by paulson
new theory PPROD
1998-11-16, by paulson
a faster proof
1998-11-16, by paulson
removed genelim.ML;
1998-11-16, by wenzelm
thm, thms;
1998-11-16, by wenzelm
added print_thm;
1998-11-16, by wenzelm
made SML/NJ happy;
1998-11-16, by wenzelm
added oo, ooo (*concatenation: 2 and 3 args*);
1998-11-16, by wenzelm
Attribute.tthms_of;
1998-11-16, by wenzelm
Attribute.tthms_of;
1998-11-16, by wenzelm
Attribute.thms_of;
1998-11-16, by wenzelm
Classical.setup, attrib_setup;
1998-11-16, by wenzelm
attrib_setup: rulify;
1998-11-16, by wenzelm
attrib_setup;
1998-11-16, by wenzelm
all modifiers turned into attributes;
1998-11-16, by wenzelm
tuned attribute names;
1998-11-16, by wenzelm
several args parsers;
1998-11-16, by wenzelm
tuned names;
1998-11-16, by wenzelm
renamed tac / etac to refine / then_refine;
1998-11-16, by wenzelm
add print_theorems;
1998-11-16, by wenzelm
add print_theorems;
1998-11-16, by wenzelm
several args parsers;
1998-11-16, by wenzelm
several args parsers;
1998-11-16, by wenzelm
removed args, args1, thm_xname;
1998-11-16, by wenzelm
replaced is_symid by is_sid;
1998-11-16, by wenzelm
renamed init_context to init;
1998-11-16, by wenzelm
renamed init_context to init;
1998-11-16, by wenzelm
structure PureIsar;
1998-11-16, by wenzelm
removed lift_modifier;
1998-11-16, by wenzelm
Attribute.thms_of;
1998-11-16, by wenzelm
Scan.read;
1998-11-16, by wenzelm
added read;
1998-11-16, by wenzelm
tuned usage of read;
1998-11-16, by wenzelm
generalized JN_empty and added reachable_SKIP
1998-11-16, by paulson
removed the reference to mesontest2.ML, itself now deleted
1998-11-16, by paulson
moved some facts about Pi from ex/PiSets to Fun.ML
1998-11-16, by paulson
prefixed op;
1998-11-14, by wenzelm
Theory.copy;
1998-11-14, by wenzelm
val copy: theory -> theory;
1998-11-14, by wenzelm
added unless, first;
1998-11-14, by wenzelm
added read_nat;
1998-11-14, by wenzelm
not needed in distribution
1998-11-13, by paulson
needed tidying desperately
1998-11-13, by paulson
qualified the name "restrict" since Fun.restrict exists too
1998-11-13, by paulson
moved Pi and -> (renamed funcset) to Fun.thy
1998-11-13, by paulson
the type of @evalcn was wrong
1998-11-13, by paulson
moved UNION_o to Fun.ML, since Fun.thy is no longer a parent of equalities
1998-11-13, by paulson
no longer loads Fun so that the Fun proofs can use equalities.thy
1998-11-13, by paulson
the function space operator
1998-11-13, by paulson
New section on advanced datatypes.
1998-11-12, by nipkow
*** empty log message ***
1998-11-12, by nipkow
mesontest2.ML was never needed in the distribution
1998-11-12, by paulson
changed inverse syntax from x-| to i(x)
1998-11-12, by paulson
proved surjI
1998-11-11, by paulson
tidied
1998-11-11, by paulson
Big simplification of proofs.
1998-11-11, by paulson
tiny changes;
1998-11-10, by mueller
changed to a link;
1998-11-10, by mueller
local simpset theory data;
1998-11-09, by wenzelm
local claset theory data;
1998-11-09, by wenzelm
Object logic specific operations.
1998-11-09, by wenzelm
Isar setups;
1998-11-09, by wenzelm
added metacuts_tac;
1998-11-09, by wenzelm
removed local_theory;
1998-11-09, by wenzelm
exnMessage Interrupt;
1998-11-09, by wenzelm
added lift_modifier, rule;
1998-11-09, by wenzelm
added Isar;
1998-11-09, by wenzelm
added Isar/;
1998-11-09, by wenzelm
Pure outer syntax.
1998-11-09, by wenzelm
Non-logical toplevel commands.
1998-11-09, by wenzelm
Derived theory operations.
1998-11-09, by wenzelm
The global Isabelle/Isar outer syntax.
1998-11-09, by wenzelm
The Isabelle/Isar toplevel.
1998-11-09, by wenzelm
Histories of proof states, with undo / redo and prev / back.
1998-11-09, by wenzelm
Generic parsers for Isabelle/Isar outer syntax.
1998-11-09, by wenzelm
Outer lexical syntax for Isabelle/Isar.
1998-11-09, by wenzelm
Proof methods.
1998-11-09, by wenzelm
Symbolic theorem attributes.
1998-11-09, by wenzelm
Concrete argument syntax (for attributes, methods etc.).
1998-11-09, by wenzelm
Type-safe interface for proof context data.
1998-11-09, by wenzelm
Proof states and methods.
1998-11-09, by wenzelm
Proof context information.
1998-11-09, by wenzelm
Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
1998-11-09, by wenzelm
Check release name and date in NEWS!
1998-11-09, by wenzelm
smart interrupt handler;
1998-11-09, by wenzelm
option -I: startup Isar interaction mode;
1998-11-09, by wenzelm
isabelle -I;
1998-11-09, by wenzelm
fake interrupt handler;
1998-11-09, by wenzelm
simple interrupt_handler;
1998-11-09, by wenzelm
new Domain/Range rules
1998-11-09, by paulson
new TIMES/Sigma rules
1998-11-09, by paulson
removed obsolete comment and "open" declaration
1998-11-09, by paulson
"Subscribe" link
1998-11-06, by paulson
spell check;
1998-11-06, by wenzelm
tuned;
1998-11-06, by wenzelm
added mailing list, removed mirrors;
1998-11-06, by mueller
Revising the Client proof as suggested by Michel Charpentier. New lemmas
1998-11-06, by paulson
made more generic;
1998-11-05, by mueller
Shortened names and added new thm.
1998-11-05, by nipkow
Some streamlining of text.
1998-11-04, by paulson
tuned;
1998-11-03, by wenzelm
tuned width of pics;
1998-11-03, by wenzelm
tuned;
1998-11-03, by wenzelm
oops;
1998-11-02, by wenzelm
tuned pics;
1998-11-02, by wenzelm
made weblint happy;
1998-11-02, by wenzelm
oops;
1998-11-02, by wenzelm
Id;
1998-11-02, by wenzelm
tuned;
1998-11-02, by wenzelm
tuned;
1998-11-02, by wenzelm
main Isabelle page;
1998-11-02, by wenzelm
New example
1998-11-02, by nipkow
Domain r, Range r replace fst``r, snd``r
1998-11-02, by paulson
increased precedence of unary minus from 80 to 100
1998-11-02, by paulson
increased precedence of unary minus from 80 to 100
1998-11-02, by paulson
Charpentier laws
1998-10-31, by paulson
the Increasing operator
1998-10-31, by paulson
no need for int_0
1998-10-31, by paulson
locales now implicitly quantify over free variables
1998-10-31, by paulson
tuned current_goals_markers;
1998-10-30, by wenzelm
Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed
1998-10-30, by paulson
Explicit (and improved) simprules for binary arithmetic.
1998-10-30, by paulson
*** empty log message ***
1998-10-29, by wenzelm
shyps note for prim. rules;
1998-10-29, by wenzelm
tuned;
1998-10-29, by wenzelm
tuned current_goals_markers semantics to avoid empty lines;
1998-10-29, by wenzelm
tidied
1998-10-29, by paulson
auto update
1998-10-29, by paulson
Some more proofs.
1998-10-28, by nipkow
added nat_diff_split and a few lemmas in Trancl.
1998-10-28, by nipkow
ML_SYSTEM=polyml-3.1;
1998-10-26, by wenzelm
tuned checklist;
Isabelle98-1
1998-10-25, by wenzelm
official release;
1998-10-24, by wenzelm
less
more
|
(0)
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip