Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-3000
-1000
-960
+960
+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.
usage: tell ISABELLE_USEDIR_OPTIONS;
1999-09-03, by wenzelm
tuned;
1999-09-03, by wenzelm
usage: tell current OPTIONS value;
1999-09-03, by wenzelm
updated;
1999-09-03, by wenzelm
fixed usepackage;
1999-09-03, by wenzelm
permuted index;
1999-09-03, by wenzelm
\PROP;
1999-09-03, by wenzelm
no_qed;
1999-09-03, by wenzelm
no_qed;
1999-09-03, by wenzelm
"this";
1999-09-03, by wenzelm
tuned;
1999-09-03, by wenzelm
added bind_thms;
1999-09-03, by wenzelm
tuned K;
1999-09-03, by wenzelm
tuned;
1999-09-03, by wenzelm
from hyp;
1999-09-03, by wenzelm
added no_qed;
1999-09-03, by wenzelm
new theorem fun_upd_upd
1999-09-03, by paulson
new SVC url
1999-09-03, by paulson
renamed NatSum to Summation;
1999-09-02, by wenzelm
tidied;
1999-09-02, by wenzelm
AddXDs [bspec];
1999-09-02, by wenzelm
added with_path;
1999-09-02, by wenzelm
terminal method: always involve finish;
1999-09-02, by wenzelm
with_path;
1999-09-02, by wenzelm
renamed improper method 'clarsimp' to 'clarsimp_tac';
1999-09-02, by wenzelm
added MultisetOrder.thy;
1999-09-01, by wenzelm
Isar_examples/MultisetOrder.thy;
1999-09-01, by wenzelm
tuned;
1999-09-01, by wenzelm
"this";
1999-09-01, by wenzelm
Wellfoundedness proof for the multiset order (preliminary version).
1999-09-01, by wenzelm
fix: vars;
1999-09-01, by wenzelm
removed "*" method combinator;
1999-09-01, by wenzelm
observe show_types;
1999-09-01, by wenzelm
bind_thms;
1999-09-01, by wenzelm
bind_thm "case";
1999-09-01, by wenzelm
*: no quotes;
1999-09-01, by wenzelm
Method.insert_tac;
1999-09-01, by wenzelm
Method.insert_tac;
1999-09-01, by wenzelm
Method.insert_tac;
1999-09-01, by wenzelm
bind_thm;
1999-09-01, by wenzelm
added bind_thms, store_thms;
1999-09-01, by wenzelm
structures Vartab / Termtab (instances of TableFun);
1999-09-01, by wenzelm
tuned;
1999-09-01, by wenzelm
any_props: improved error;
1999-09-01, by wenzelm
fix: common constraints;
1999-09-01, by wenzelm
Thm.def_name;
1999-09-01, by wenzelm
replaced IsarCmd.kill_theory by Toplevel.kill;
1999-09-01, by wenzelm
calculation: thm list;
1999-09-01, by wenzelm
removed kill_theory;
1999-09-01, by wenzelm
removed the_fact;
1999-09-01, by wenzelm
fix: common constraints;
1999-09-01, by wenzelm
added store/bind_thms;
1999-09-01, by wenzelm
added theorems;
1999-09-01, by wenzelm
added theorems;
1999-09-01, by wenzelm
isar: avoid verbose goal responses;
1999-09-01, by wenzelm
structure Termtab;
1999-09-01, by wenzelm
smart_store_thms;
1999-09-01, by wenzelm
PureThy.smart_store_thms;
1999-09-01, by wenzelm
tidied some proofs
1999-09-01, by paulson
tidied
1999-09-01, by paulson
tidied
1999-08-31, by paulson
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
1999-08-31, by paulson
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
1999-08-31, by paulson
proper calculation / induction;
1999-08-30, by wenzelm
tuned;
1999-08-30, by wenzelm
OF: "_" as argument;
1999-08-30, by wenzelm
clean: include HOL-Real-ex;
1999-08-30, by wenzelm
auto: CHANGED;
1999-08-30, by wenzelm
make it actually RUN the real examples
1999-08-30, by paulson
new directory HOL/Real/ex of real examples
1999-08-30, by paulson
'iff' attribute;
1999-08-30, by wenzelm
'arith' method;
1999-08-30, by wenzelm
'_' theorem;
1999-08-30, by wenzelm
tuned;
1999-08-30, by wenzelm
new results for localTo
1999-08-30, by paulson
a new theorem
1999-08-30, by paulson
tuned;
1999-08-30, by wenzelm
added MutilatedCheckerboard;
1999-08-29, by wenzelm
added Isar_examples/MutilatedCheckerboard.thy;
1999-08-29, by wenzelm
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
1999-08-29, by wenzelm
tuned;
1999-08-27, by wenzelm
thm "_" = asm_rl;
1999-08-27, by wenzelm
tidied
1999-08-27, by paulson
use of bij, new theorems, etc.
1999-08-27, by paulson
the bij predicate forced renaming of a variable bij
1999-08-27, by paulson
tidied, allowing pattern-matching in defs of prat_add and prat_mult
1999-08-27, by paulson
tidied, allowing pattern-matching in defs of zadd and zmult
1999-08-27, by paulson
the bij predicate (at last)
1999-08-27, by paulson
better timing information;
1999-08-27, by wenzelm
oops;
1999-08-27, by wenzelm
*** empty log message ***
1999-08-27, by wenzelm
tuned;
1999-08-26, by wenzelm
iff_attrib_setup;
1999-08-26, by wenzelm
improved back, help;
1999-08-26, by wenzelm
print_help;
1999-08-26, by wenzelm
back: recur flag;
1999-08-26, by wenzelm
a bit further with property (1)
1999-08-26, by paulson
changed "guar" back to "guarantees" (sorry) and FIXED ITS PRECEDENCE
1999-08-26, by paulson
new destruction rules
1999-08-26, by paulson
new laws; changed "guar" back to "guarantees" (sorry)
1999-08-26, by paulson
changed "guar" back to "guarantees" (sorry)
1999-08-26, by paulson
more Join rules including AC-rules
1999-08-26, by paulson
extra syntax for JN, making it more like UN
1999-08-26, by paulson
a little tidying; also FIXED BAD TYPE in INTER1, UNION1
1999-08-26, by paulson
proper bootstrap of HOL theory and packages;
1999-08-25, by wenzelm
expand_classes renamed to intro_classes;
1999-08-25, by wenzelm
proper bootstrap of IFOL/FOL theories and packages;
1999-08-25, by wenzelm
proper setup of GlobalClaset data;
1999-08-25, by wenzelm
improved msg;
1999-08-25, by wenzelm
fixed arity;
1999-08-25, by wenzelm
expand_classes renamed to intro_classes;
1999-08-25, by wenzelm
TPHOLs99;
1999-08-25, by wenzelm
Removed "Adding axioms ..." message.
1999-08-25, by berghofe
hide private parts;
1999-08-25, by wenzelm
another snapshot
1999-08-25, by paulson
arguably clearer definition of the inductive case of
1999-08-25, by paulson
tidied
1999-08-25, by paulson
new guarantees laws; also better natural deduction style for old ones
1999-08-25, by paulson
renamed some theorems; also better natural deduction style for old ones
1999-08-25, by paulson
project constants
1999-08-25, by paulson
many "project" laws
1999-08-25, by paulson
new guarantees laws; also better natural deduction style for old ones
1999-08-25, by paulson
split_paired_Eps and lemmas
1999-08-25, by paulson
new theorem inv_f_eq
1999-08-25, by paulson
%dir;
1999-08-24, by wenzelm
tuned;
1999-08-24, by wenzelm
draft release;
1999-08-24, by wenzelm
Real/Real.thy main entry point;
1999-08-24, by wenzelm
isar: no_pos flag;
1999-08-24, by wenzelm
fixed add_sect etc.;
1999-08-24, by wenzelm
??thesis: include params;
1999-08-24, by wenzelm
print_mode activated again;
1999-08-24, by wenzelm
fixed intro_elim_tac;
1999-08-24, by wenzelm
record_simproc;
1999-08-23, by wenzelm
tuned;
1999-08-23, by wenzelm
record_simproc;
1999-08-23, by wenzelm
Some changes in sections about Sum and Nat.
1999-08-23, by berghofe
simplifier flex heads.
1999-08-23, by nipkow
Now rewrite rules with flexible heads are allowed.
1999-08-23, by nipkow
isatool expandshort;
1999-08-23, by wenzelm
tuned;
1999-08-23, by wenzelm
Moved sum_case to theory HOL/Datatype.
1999-08-23, by berghofe
tuned;
1999-08-23, by wenzelm
Corrected two busg in the simplifier.
1999-08-23, by nipkow
\indexisarreg;
1999-08-22, by wenzelm
\VVar;
1999-08-22, by wenzelm
checkpoint;
1999-08-22, by wenzelm
tuned;
1999-08-22, by wenzelm
real numerals;
1999-08-21, by wenzelm
added HOL-Real;
1999-08-21, by wenzelm
echo ML_PLATFORM;
1999-08-20, by wenzelm
activate example;
1999-08-20, by wenzelm
delcongs [if_weak_cong];
1999-08-20, by wenzelm
print_context;
1999-08-20, by wenzelm
eliminated HOL-AxClasses target;
1999-08-20, by wenzelm
intro (no +);
1999-08-20, by wenzelm
mucke -res;
1999-08-20, by wenzelm
if_svc_enabled;
1999-08-20, by wenzelm
AxClasses, Isar_examples;
1999-08-20, by wenzelm
intro/elim: REPEAT1;
1999-08-20, by wenzelm
new theories RealBin, RealInt, RealPow
1999-08-20, by paulson
* HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with HOL/List;
1999-08-19, by wenzelm
quite a lot of tuning and cleanup;
1999-08-19, by wenzelm
sysman: Stefan Berghofer;
1999-08-19, by wenzelm
more;
1999-08-19, by wenzelm
Mucke, Einhoven;
1999-08-19, by wenzelm
quite a lot of tuning an cleanup;
1999-08-19, by wenzelm
sum_case_Inl and sum_case_Inr are now defined in Datatype.ML.
1999-08-19, by berghofe
Moved sum_case stuff from Sum to Datatype.
1999-08-19, by berghofe
real literals using binary arithmetic
1999-08-19, by paulson
new entriues.
1999-08-19, by nipkow
updated
1999-08-19, by paulson
disabled print_mode (tmp);
1999-08-19, by wenzelm
lookup_theory;
1999-08-19, by wenzelm
defer_recdef
1999-08-19, by paulson
removed needless comments
1999-08-19, by paulson
removed all unnecessary code
1999-08-19, by paulson
now with abstraction code previously in HOL/Tools/svc_funcs.ML
1999-08-19, by paulson
documented svc_tac
1999-08-19, by paulson
finished theories;
1999-08-19, by wenzelm
renamed 'some_rule' to 'rule';
1999-08-19, by wenzelm
tuned;
1999-08-19, by wenzelm
removed fixnumerals (for the time being);
1999-08-19, by wenzelm
tuned Goal syntax;
1999-08-19, by wenzelm
improved messages;
1999-08-19, by wenzelm
really removed -m option;
1999-08-19, by wenzelm
removed -m option;
1999-08-19, by wenzelm
usedir: removed -m option;
1999-08-19, by wenzelm
Method.modifier;
1999-08-18, by wenzelm
Method.modifier;
1999-08-18, by wenzelm
assume: multiple args;
1999-08-18, by wenzelm
warn_vars;
1999-08-18, by wenzelm
assume/presume: and_list1;
1999-08-18, by wenzelm
sectioned_args etc.: more general modifier;
1999-08-18, by wenzelm
deps: include 'really' flag;
1999-08-18, by wenzelm
isa_action: don't lock pretend_used files;
1999-08-18, by wenzelm
proper writeln of begin_state;
1999-08-18, by wenzelm
(*no fix_shyps*);
1999-08-18, by wenzelm
tuned messages;
1999-08-18, by wenzelm
from Konrad: support for schematic definitions
1999-08-18, by paulson
sum_case renamed to basic_sum_case;
1999-08-18, by wenzelm
Removed rbeta.
1999-08-18, by berghofe
tuned messages;
1999-08-18, by wenzelm
tuned;
1999-08-18, by wenzelm
Renamed sum_case to basic_sum_case.
1999-08-18, by berghofe
Eliminated some infixes.
1999-08-18, by berghofe
Eliminated some infixes.
1999-08-18, by berghofe
Renamed sum_case to basic_sum_case and removed translations for sum_case
1999-08-18, by berghofe
tuned;
1999-08-18, by wenzelm
replaced 'ProofGeneral' by 'Proof General';
1999-08-18, by wenzelm
Modified section about generation of theory browsing information.
1999-08-18, by berghofe
new version from Konrad with "lazy" (deferred) definitons
1999-08-18, by paulson
tidied some proofs
1999-08-18, by paulson
new primitive rule permute_prems to underlie defer_tac and rotate_prems
1999-08-18, by paulson
freeze_thaw does nothing if no variables
1999-08-18, by paulson
Added take_all and drop_all to simpset.
1999-08-18, by nipkow
eliminated HOL_quantifiers (replaced by "HOL" print mode);
1999-08-17, by wenzelm
may_load_file;
1999-08-17, by wenzelm
ThyInfo.may_load_file;
1999-08-17, by wenzelm
begin_update_theory;
1999-08-17, by wenzelm
PASS(_MODE): works better without space (why?);
1999-08-17, by wenzelm
removed HOL_quantifiers;
1999-08-17, by wenzelm
HOL_quantifiers;
1999-08-17, by wenzelm
replaced HOL_quantifiers flag by "HOL" print mode;
1999-08-17, by wenzelm
turned SVC_Oracle into a new-style theory in order to get automatic
1999-08-17, by wenzelm
Better handling of path for remote theory browsing information.
1999-08-17, by berghofe
Goals.reset_goals;
1999-08-17, by wenzelm
reset_goals;
1999-08-17, by wenzelm
intro+;
1999-08-17, by wenzelm
remove tmp files;
1999-08-17, by wenzelm
tuned;
1999-08-17, by wenzelm
renamed 'single' to 'some_rule';
1999-08-17, by wenzelm
renamed Cons to Consq in order to avoid clash with List.Cons;
1999-08-17, by wenzelm
Tuned some comments.
1999-08-17, by berghofe
Path for remote theory browsing information is now stored in referece variable rpath.
1999-08-17, by berghofe
-m option;
1999-08-17, by wenzelm
replaced "op #" by "Cons";
1999-08-16, by wenzelm
'a list: Nil, Cons;
1999-08-16, by wenzelm
tuned msg;
1999-08-16, by wenzelm
disable_pr, enable_pr;
1999-08-16, by wenzelm
deleted obsolete assignment
1999-08-16, by paulson
restored a high precedence to unary minus
1999-08-16, by paulson
inserted Id: lines
1999-08-16, by paulson
new theory Real/Hyperreal/HyperDef and file fuf.ML
1999-08-16, by paulson
forgot to write back adaption of onlysimps
1999-08-16, by oheimb
tuned;
1999-08-16, by wenzelm
tuned;
1999-08-16, by wenzelm
exchanged finish_tac and unsafe_finish_tac (the more important one) in simpset
1999-08-16, by oheimb
re-added refl in safe_solver
1999-08-16, by oheimb
removed warn_theory_style;
1999-08-16, by wenzelm
fixed thy_only;
1999-08-16, by wenzelm
tuned prompts;
1999-08-16, by wenzelm
isamode;
1999-08-16, by wenzelm
user infaces: tuned, added ProofGeneral;
1999-08-16, by wenzelm
bib;
1999-08-16, by wenzelm
-m option;
1999-08-16, by wenzelm
Tuned.
1999-08-12, by berghofe
Removed
1999-08-11, by nipkow
* set HOL_quantifiers by default, i.e. quantifiers are printed as
1999-08-11, by nipkow
added asym rule;
1999-08-09, by wenzelm
tuned print_state;
1999-08-09, by wenzelm
tuned strings_of_context;
1999-08-09, by wenzelm
pr / no_pr: maintain Toplevel.quiet;
1999-08-09, by wenzelm
tuned print_state;
1999-08-09, by wenzelm
append user rules;
1999-08-09, by wenzelm
theory loader actions;
1999-08-09, by wenzelm
made SML happy;
1999-08-06, by wenzelm
tuned;
1999-08-06, by wenzelm
proper ProofGeneral/isa setup;
1999-08-06, by wenzelm
simplified ML handling;
1999-08-06, by wenzelm
added pretend_use;
1999-08-06, by wenzelm
simplified handling of ML file;
1999-08-06, by wenzelm
the whole file is now loaded only if SVC is enabled
1999-08-06, by paulson
re-organization of theorems from Alloc and PPROD, partly into new theory
1999-08-06, by paulson
svc_enabled is now declared as a function
1999-08-06, by paulson
new theory UNITY/Lift_prog
1999-08-06, by paulson
External reasoning tools;
1999-08-06, by wenzelm
no longer gives a default value to SVC_MACHINE
1999-08-06, by paulson
extra comment
1999-08-06, by paulson
now catches exn THEORY and prints an error message
1999-08-06, by paulson
some hard propositional examples
1999-08-06, by paulson
new theory ex/svc_test.thy
1999-08-06, by paulson
removed obsolete addsimps update_defs;
1999-08-05, by wenzelm
record_simproc for sel-upd (by Sebastian Nanz);
1999-08-05, by wenzelm
change_simpset_of;
1999-08-05, by wenzelm
local goals: after_qed;
1999-08-05, by wenzelm
tuned;
1999-08-04, by wenzelm
added isabelle-sys, proofgeneral;
1999-08-04, by wenzelm
improved \NOTE;
1999-08-04, by wenzelm
tuned;
1999-08-03, by wenzelm
improved interest;
1999-08-03, by wenzelm
tuned;
1999-08-03, by wenzelm
tuned attdx, methdx;
1999-08-03, by wenzelm
fixed {};
1999-08-03, by wenzelm
tuned;
1999-08-03, by wenzelm
Sara Kalvala: moving the <<...>> notation from LK to Sequents
1999-08-03, by paulson
new examples file for SVC
1999-08-03, by paulson
biconditionals and the natural numbers
1999-08-03, by paulson
added realT
1999-08-03, by paulson
biconditionals and the natural numbers
1999-08-03, by paulson
new examples file for SVC
1999-08-03, by paulson
new chapter on Sequents
1999-08-03, by paulson
\underscoreoff needed because of \underscoreon in previous file
1999-08-03, by paulson
new variables for SVC
1999-08-03, by paulson
SVC
1999-08-03, by paulson
fixed Blast_Data;
1999-08-02, by wenzelm
blast method: optional depth argument;
1999-08-02, by wenzelm
export cla_meth(');
1999-08-02, by wenzelm
tuned;
1999-08-02, by wenzelm
tuned outer syntax;
1999-08-02, by wenzelm
handle LIST _;
1999-08-02, by wenzelm
cat_lines;
1999-08-02, by wenzelm
provide String structure;
1999-08-02, by wenzelm
removed obsolete concat;
1999-08-02, by wenzelm
String.isPrefix
1999-08-02, by paulson
long-overdue updating
1999-08-02, by paulson
new files for the SVC link-up
1999-08-02, by paulson
the SVC oracle theory
1999-08-02, by paulson
the SVC link-up
1999-08-02, by paulson
new files for the SVC link-up
1999-08-02, by paulson
even more stuff;
1999-07-30, by wenzelm
oracle: '=';
1999-07-30, by wenzelm
added \text;
1999-07-30, by wenzelm
Isabelle/Isar macros;
1999-07-30, by wenzelm
hacking the rail package;
1999-07-30, by wenzelm
added update_thy_only;
1999-07-30, by wenzelm
more;
1999-07-30, by wenzelm
more stuff;
1999-07-30, by wenzelm
renamed 'same' to '-';
1999-07-30, by wenzelm
eliminated METHOD0 in favour of same_tac;
1999-07-30, by wenzelm
'arith' proof method;
1999-07-30, by wenzelm
added erule;
1999-07-30, by wenzelm
export sysify_path;
1999-07-30, by wenzelm
split_diff and remove_diff_ss
1999-07-30, by paulson
added parentheses to cope with a possible reduction of the precedence of unary
1999-07-29, by paulson
ML_HOME=$ISABELLE_HOME/../smlnj/bin;
1999-07-28, by wenzelm
HOL-Real target now builds an actual image;
1999-07-28, by wenzelm
added pretty_setmargin;
1999-07-28, by wenzelm
congruence rule for |-, etc.
1999-07-28, by paulson
renamed ...thm_pack... to ...pack...
1999-07-28, by paulson
removed the unused SeqVar option
1999-07-28, by paulson
sequents require higher bounds
1999-07-28, by paulson
more examples are working
1999-07-28, by paulson
adding missing declarations for the <<...>> notation
1999-07-28, by paulson
congruence rule for |-
1999-07-28, by paulson
simplifier and improved classical reasoner
1999-07-28, by paulson
mkdir contrib;
1999-07-28, by wenzelm
added String.concat
1999-07-28, by paulson
LK
1999-07-28, by paulson
back again, supposedly with correct perms;
1999-07-27, by wenzelm
*** empty log message ***
1999-07-27, by wenzelm
fixed perms and final nl;
1999-07-27, by wenzelm
fixed comments;
1999-07-27, by wenzelm
fixed comment;
1999-07-27, by wenzelm
inductive_cases(_i): Isar interface to mk_cases;
1999-07-27, by wenzelm
safe_step_tac / step_tac;
1999-07-27, by wenzelm
init / init_theory: pass int flag;
1999-07-27, by wenzelm
added thy_switch kind;
1999-07-27, by wenzelm
removed update_context;
1999-07-27, by wenzelm
removed update_context;
1999-07-27, by wenzelm
removed restart;
1999-07-27, by wenzelm
setup_thy_loader;
1999-07-27, by wenzelm
added update_thy_only;
1999-07-27, by wenzelm
installation of simplifier and classical reasoner, better rules etc
1999-07-27, by paulson
moved the modal prover to modal.ML; installed the prover using TheoryDataFun
1999-07-27, by paulson
split off modal.ML from provers.ML
1999-07-27, by paulson
fixed the comments...
1999-07-27, by paulson
a new theory containing just an axiom needed to derive imp_cong
1999-07-27, by paulson
renamed theory LK to LK0
1999-07-27, by paulson
renamed LK0.ML
1999-07-27, by paulson
Sequents/LK/Nat: new example of simplification in LK
1999-07-27, by paulson
added gen_inter
1999-07-27, by paulson
expandshort and tidying
1999-07-27, by paulson
expandshort; tidied
1999-07-27, by paulson
tidied
1999-07-27, by paulson
expandshort
1999-07-26, by paulson
HOL/ex/Tarski: new example by Florian Kammueller
1999-07-26, by paulson
new facts about binomials
1999-07-26, by paulson
three new theorems
1999-07-26, by paulson
new cancellation laws
1999-07-26, by paulson
tidied
1999-07-26, by paulson
new simprocs assoc_fold and combine_coeff
1999-07-23, by paulson
removed the combine_coeff simproc because linear arith does not handle
1999-07-23, by paulson
now using correctly-typed constants from HOLogic
1999-07-23, by paulson
heavily revised by Jacques: coercions have alphabetic names;
1999-07-23, by paulson
because intT is now defined in HOLogic
1999-07-23, by paulson
zmult_ac are no longer included by default
1999-07-23, by paulson
zadd_ac and zmult_ac are no longer included by default
1999-07-23, by paulson
added boolean and binary constants
1999-07-23, by paulson
new simprocs assoc_fold and combine_coeff
1999-07-23, by paulson
rail -a;
1999-07-23, by wenzelm
tuned add_term_varnames;
1999-07-23, by wenzelm
replaced assoc lists by Symtab.table;
1999-07-23, by wenzelm
Type.norm_term;
1999-07-23, by wenzelm
replace assoc lists by Symtab.table;
1999-07-23, by wenzelm
require_thy: fixed performance leak;
1999-07-23, by wenzelm
fix occurences of numerals in HOL/ZF terms;
1999-07-23, by wenzelm
New lemmas by Stefan Merz.
1999-07-23, by nipkow
avoid '(0 subgoals)';
1999-07-22, by wenzelm
Toplevel.excursion_error;
1999-07-22, by wenzelm
added exists;
1999-07-22, by wenzelm
Tuned.
1999-07-22, by berghofe
a stronger diff_less and no more le_diff_less
1999-07-21, by paulson
removed 2 qed_goals
1999-07-21, by paulson
tweaked proofs to handle new freeness reasoning for data c onstructors
1999-07-21, by paulson
more existing theorems renamed to use #0; also new results
1999-07-21, by paulson
now exports mk_bin
1999-07-21, by paulson
a more robust proof
1999-07-21, by paulson
tweaked proof after removal of diff_is_0_eq RS iffD2
1999-07-21, by paulson
better error message for curried recdefs, etc.
1999-07-21, by paulson
Mod by Norber Voelcker
1999-07-21, by nipkow
checkpoint;
1999-07-20, by wenzelm
Eliminated addDistinct.
1999-07-20, by berghofe
facts: no statement_binds;
1999-07-19, by wenzelm
Datatype package now handles arbitrarily branching datatypes.
1999-07-19, by berghofe
skeleton only;
1999-07-19, by wenzelm
added isar-ref;
1999-07-19, by wenzelm
Documented usage of function types in datatype specifications.
1999-07-19, by berghofe
added attdx, methdx;
1999-07-19, by wenzelm
added isabelle_isar logo;
1999-07-19, by wenzelm
updated;
1999-07-19, by wenzelm
renamed 'with' to 'using';
1999-07-19, by wenzelm
*** empty log message ***
1999-07-19, by wenzelm
NatBin: binary arithmetic for the naturals
1999-07-19, by paulson
examples of arithmetic on the naturals
1999-07-19, by paulson
deleted a reference to "nat", now erroneous because "nat" is a function
1999-07-19, by paulson
many new laws about div and mod
1999-07-19, by paulson
new theorem zless_zero_nat
1999-07-19, by paulson
removal of rewrites for Suc(Suc(Suc...)))
1999-07-19, by paulson
NatBin: binary arithmetic for the naturals
1999-07-19, by paulson
getting rid of qed_goal
1999-07-19, by paulson
getting rid of qed_goal
1999-07-19, by paulson
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
1999-07-19, by paulson
Modifid length_tl
1999-07-18, by nipkow
adapted to dest_keywords, dest_parsers;
1999-07-16, by wenzelm
separate command tokens;
1999-07-16, by wenzelm
tuned dest_lexicon;
1999-07-16, by wenzelm
tuned;
1999-07-16, by wenzelm
removed break;
1999-07-16, by wenzelm
removed BREAK, ROLLBACK;
1999-07-16, by wenzelm
structure LocalDefs = LocalDefs;
1999-07-16, by wenzelm
Exported function unify_consts (workaround to avoid inconsistently
1999-07-16, by berghofe
Added new example (infinitely branching trees).
1999-07-16, by berghofe
Infinitely branching trees.
1999-07-16, by berghofe
Replaced datatype_info by datatype_info_err.
1999-07-16, by berghofe
- Now also supports arbitrarily branching datatypes.
1999-07-16, by berghofe
- Datatype package now also supports arbitrarily branching datatypes
1999-07-16, by berghofe
Added some definitions and theorems needed for the
1999-07-16, by berghofe
Some rather large datatype examples (from John Harrison).
1999-07-16, by berghofe
improved print_thms;
1999-07-15, by wenzelm
export init_state;
1999-07-15, by wenzelm
more renaming of theorems from _nat to _int (corresponding to a function that
1999-07-15, by paulson
more renaming of theorems from _nat to _int (corresponding to a function that
1999-07-15, by paulson
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
1999-07-15, by paulson
qed_goal -> Goal
1999-07-15, by paulson
tuned;
1999-07-14, by wenzelm
tuned comments;
1999-07-14, by wenzelm
tuned contradiction method;
1999-07-14, by wenzelm
improved comment;
1999-07-14, by wenzelm
more marg_comments;
1999-07-14, by wenzelm
Deriving rules in Isabelle;
1999-07-14, by wenzelm
rewrite add1_zle_eq is no longer in the default simpset
1999-07-14, by paulson
optimization for division by powers of 2
1999-07-14, by paulson
new montonicity theorems
1999-07-14, by paulson
new constant folding rewrites
1999-07-14, by paulson
handle cgoal;
1999-07-13, by wenzelm
added mk_cgoal, assume_goal;
1999-07-13, by wenzelm
same_tac;
1999-07-13, by wenzelm
change to force (m div 0 = 0)
1999-07-13, by paulson
many new theorems
1999-07-13, by paulson
renamed inj_nat to inj_int
1999-07-13, by paulson
new monotonicity theorems
1999-07-13, by paulson
new theorem zmult_eq_0_iff
1999-07-13, by paulson
renamed sort "numeral" to "number"
1999-07-13, by paulson
simplified the <= monotonicity proof
1999-07-13, by paulson
local qeds: print rule;
1999-07-12, by wenzelm
added show_hyps flag;
1999-07-12, by wenzelm
local qed; print rule;
1999-07-12, by wenzelm
term/prop: include number;
1999-07-12, by wenzelm
added show_hyps flag;
1999-07-12, by wenzelm
export assumption_tac;
1999-07-12, by wenzelm
removed merge_theories;
1999-07-12, by wenzelm
removed metacuts_tac;
1999-07-12, by wenzelm
tmp_path: *add* path;
1999-07-12, by wenzelm
thms_containing: undeclared consts error;
1999-07-12, by wenzelm
removed pretty_thm_no_hyps (again);
1999-07-12, by wenzelm
removed merge_theories;
1999-07-12, by wenzelm
may get BASH_PATH etc. from env;
1999-07-12, by wenzelm
new theorems for the "at most" relation
1999-07-12, by paulson
def: ==;
1999-07-12, by wenzelm
tuned Interrupt msgs;
1999-07-10, by wenzelm
pass exn;
1999-07-10, by wenzelm
handle THM exn;
1999-07-10, by wenzelm
handle THM/TERM exn;
1999-07-10, by wenzelm
dup_elim: use try to handle general exn;
1999-07-10, by wenzelm
handle THM exn;
1999-07-10, by wenzelm
fixed interrupts (eliminated races);
1999-07-10, by wenzelm
defer_tac: use try for general exn handling;
1999-07-10, by wenzelm
Symtab.lookup_multi;
1999-07-10, by wenzelm
more specific exn;
1999-07-10, by wenzelm
err_method: pass exn;
1999-07-10, by wenzelm
prove_goalw_cterm_general: pass exeption;
1999-07-10, by wenzelm
try/can: pass Interrupt and ERROR;
1999-07-10, by wenzelm
rmdir pdf;
1999-07-09, by wenzelm
mono: extra I/E;
1999-07-09, by wenzelm
mono: AddXI/Es;
1999-07-09, by wenzelm
type claset: added extra I/E rules;
1999-07-09, by wenzelm
added Isar/local_defs.ML;
1999-07-09, by wenzelm
added 'def';
1999-07-09, by wenzelm
added local_def(_i);
1999-07-09, by wenzelm
global_qed: removed alt_name, alt_att;
1999-07-09, by wenzelm
global_qed: removed alt_name, alt_att;
1999-07-09, by wenzelm
added termp;
1999-07-09, by wenzelm
COMP: optional position;
1999-07-09, by wenzelm
write_keywords: default file name;
1999-07-09, by wenzelm
added compose_single;
1999-07-09, by wenzelm
added HOL.trans;
1999-07-09, by wenzelm
removed qed_with;
1999-07-09, by wenzelm
faster division algorithm; monotonicity of div in 2nd arg
1999-07-09, by paulson
more monotonicity laws for times
1999-07-09, by paulson
products of signs as equivalences
1999-07-09, by paulson
-B option;
1999-07-08, by wenzelm
removed old version;
1999-07-08, by wenzelm
tuned indentation;
1999-07-08, by wenzelm
added export_chain;
1999-07-08, by wenzelm
propp: 'concl' patterns;
1999-07-08, by wenzelm
propp: 'concl' patterns;
1999-07-08, by wenzelm
terminal_proof: 2nd method;
1999-07-08, by wenzelm
'export';
1999-07-08, by wenzelm
propp: 'concl' patterns;
1999-07-08, by wenzelm
propp: 'concl' patterns;
1999-07-08, by wenzelm
improved error msgs of cterm_instantiate;
1999-07-08, by wenzelm
aprop: ??id, ...;
1999-07-08, by wenzelm
improved error msgs of instantiate;
1999-07-08, by wenzelm
added commute: 'a seq list -> 'a list seq;
1999-07-08, by wenzelm
added pretty_thm_no_hyps;
1999-07-08, by wenzelm
theorems involving oracles are now printed with a suffixed [!];
1999-07-08, by wenzelm
Theorems involving oracles will be printed with a suffixed \verb|[!]|;
1999-07-08, by wenzelm
updated usedir;
1999-07-08, by wenzelm
integer division
1999-07-08, by paulson
Renaming of theorems from _nat0 to _int0 and _nat1 to _int1
1999-07-08, by paulson
Introduction of integer division algorithm
1999-07-08, by paulson
changed header to cope with default if_weak_cong
1999-07-08, by paulson
Now if_weak_cong is a standard congruence rule
1999-07-08, by paulson
Introduction of integer division algorithm
1999-07-08, by paulson
tidied proofs to cope with default if_weak_cong
1999-07-08, by paulson
Now if_weak_cong is a standard congruence rule
1999-07-08, by paulson
new theory IntDiv.thy
1999-07-08, by paulson
new files IntDiv.{thy,ML}
1999-07-08, by paulson
tuned output;
1999-07-07, by wenzelm
simp only: attribute, method arg;
1999-07-06, by wenzelm
use generic numeral encoding and syntax;
1999-07-06, by wenzelm
adapted to generic numerals;
1999-07-06, by wenzelm
simp only;
1999-07-06, by wenzelm
added Numeral.thy;
1999-07-06, by wenzelm
_reflcl;
1999-07-06, by wenzelm
added Numeral.thy, Tools/numeral_syntax.ML;
1999-07-06, by wenzelm
removed proof history nesting commands (not useful);
1999-07-06, by wenzelm
improved errors;
1999-07-06, by wenzelm
removed nesting (unused);
1999-07-06, by wenzelm
export term_of_typ;
1999-07-06, by wenzelm
begin_theory: disallow finished;
1999-07-06, by wenzelm
added clear_mss;
1999-07-06, by wenzelm
variant version;
1999-07-05, by wenzelm
fixed scope of x:??H;
1999-07-04, by wenzelm
close_block: transfer_used_names;
1999-07-04, by wenzelm
added transfer_used_names;
1999-07-04, by wenzelm
oops;
1999-07-03, by wenzelm
proper text;
1999-07-03, by wenzelm
tuned;
1999-07-03, by wenzelm
tuned print_state;
1999-07-03, by wenzelm
fixed 'txt';
1999-07-03, by wenzelm
pretty_thm: include oracles (!) in hyps;
1999-07-03, by wenzelm
skip_proof feature 'sorry' (for quick_and_dirty mode only);
1999-07-02, by wenzelm
generalized fixes get index 0;
1999-07-02, by wenzelm
added 'txt';
1999-07-02, by wenzelm
add_txt;
1999-07-02, by wenzelm
tuned;
1999-07-02, by wenzelm
fixed order_trans;
1999-07-01, by wenzelm
added KnasterTarski.thy;
1999-07-01, by wenzelm
renamed with/APP to of/OF;
1999-07-01, by wenzelm
Isar_examples/KnasterTarski.thy;
1999-07-01, by wenzelm
added with_facts(_i);
1999-07-01, by wenzelm
'with' as == 'from' as facts;
1999-07-01, by wenzelm
also, finally: opt_rules;
1999-07-01, by wenzelm
have_thmss: more_ths;
1999-07-01, by wenzelm
have_thmss: more_ths;
1999-07-01, by wenzelm
renamed with/APP to of/OF;
1999-07-01, by wenzelm
tuned;
1999-07-01, by wenzelm
fixed backtracking of global_qed;
1999-07-01, by wenzelm
added check_result;
1999-07-01, by wenzelm
setmp Display.show_hyps false;
1999-07-01, by wenzelm
fix, assume, presume: prf_asm;
1999-07-01, by wenzelm
added prf_asm;
1999-07-01, by wenzelm
expandshort
1999-07-01, by paulson
many new theorems concerning multiplication and (in)equations
1999-07-01, by paulson
now div and mod are overloaded; dvd is polymorphic
1999-07-01, by paulson
new laws mult_le_cancel1, mult_le_cancel2
1999-07-01, by paulson
antisym first;
1999-06-30, by wenzelm
more robust trans rules;
1999-06-30, by wenzelm
Isar.sync_main;
1999-06-30, by wenzelm
added sync;
1999-06-30, by wenzelm
sync token;
1999-06-30, by wenzelm
sync;
1999-06-30, by wenzelm
added sync marker;
1999-06-30, by wenzelm
New thm trancl_trans_induct
1999-06-30, by nipkow
Bad translation fixed.
1999-06-29, by nipkow
updated;
1999-06-28, by wenzelm
improved RANGE;
1999-06-28, by wenzelm
tuned;
1999-06-28, by wenzelm
cond_extern_table;
1999-06-28, by wenzelm
added presume command;
1999-06-28, by wenzelm
cond_extern_table;
1999-06-28, by wenzelm
tuned print_state;
1999-06-28, by wenzelm
tuned output: print_context replaced by strings_of_context;
1999-06-28, by wenzelm
cond_extern_table;
1999-06-28, by wenzelm
added cond_extern_table;
1999-06-28, by wenzelm
branching_level = 400;
1999-06-25, by wenzelm
tidied
1999-06-23, by paulson
renamed PPI to plam
1999-06-23, by paulson
renamed PPI to plam
1999-06-23, by paulson
another non-working snapshot
1999-06-23, by paulson
new distributive laws involving * and -
1999-06-23, by paulson
rewrite rules to distribute CONSTANT multiplication over sum and difference;
1999-06-23, by paulson
another snapshot, still not working
1999-06-17, by paulson
new results about SKIP
1999-06-17, by paulson
addition of drop_... operators with new results and simplification of old ones
1999-06-17, by paulson
renamed UNION_... to UN_..., INTER_... to INT_... (to fit the convention)
1999-06-17, by paulson
many new guarantees laws
1999-06-17, by paulson
moved image_UNION to Fun/image_UN
1999-06-17, by paulson
expandshort
1999-06-17, by paulson
renamed UNION_... to UN_... (to fit the convention)
1999-06-17, by paulson
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
1999-06-17, by paulson
not working but taking shape
1999-06-13, by paulson
guar; locale for the spec
1999-06-13, by paulson
many new results for reachable and lift_prog
1999-06-13, by paulson
new finiteness theorems
1999-06-13, by paulson
renamed pfix_[lg}e
1999-06-13, by paulson
new-style infix directives
1999-06-13, by paulson
guarantees -> guar
1999-06-13, by paulson
guarantees -> juar
1999-06-13, by paulson
rev=rev lemma.
1999-06-11, by nipkow
fixed title line; added spacing
1999-06-11, by paulson
no longer needs ../Lex
1999-06-11, by paulson
new UNITY files
1999-06-11, by paulson
unclosed comment.
1999-06-10, by nipkow
The Allocator example: specifications
1999-06-10, by paulson
expandshort
1999-06-10, by paulson
many new lemmas about take & drop, incl the famous take-lemma
1999-06-10, by paulson
moved predicates refl, sym down to Relation.thy
1999-06-10, by paulson
Always_LeadsTo_pre. Always_LeadsTo_post: new equivalences suggested by Misra
1999-06-10, by paulson
using the new GenPrefix theory
1999-06-10, by paulson
shortened Follows to Fols
1999-06-10, by paulson
tidied
1999-06-10, by paulson
new translation to allow images over Nonce
1999-06-10, by paulson
new preficates refl, sym [from Integ/Equiv], antisym
1999-06-10, by paulson
new lemma less_Suc_eq_0_disj
1999-06-10, by paulson
Generalized prefix theory, replacing the reference to directory Lex.
1999-06-10, by paulson
Stefan Merz's lemmas.
1999-06-09, by nipkow
added square root example.
1999-06-08, by nipkow
renamed the underlying relation of leadsTo from "leadsto"
1999-06-08, by paulson
removed obsolete "Prefix" ancestor
1999-06-08, by paulson
new classical example from Lewis Carroll via S G Pulman
1999-06-08, by paulson
tuned mode_name;
1999-06-07, by wenzelm
improved handling of assumptions;
1999-06-07, by wenzelm
facts: bind named props (from proof.ML/let_thms);
1999-06-07, by wenzelm
reset HOL_quantifiers by default;
1999-06-07, by wenzelm
Added lots of 'replicate' lemmas.
1999-06-07, by nipkow
groups as monoids;
1999-06-05, by wenzelm
tuned comments;
1999-06-05, by wenzelm
added Ord.order_antisym;
1999-06-05, by wenzelm
auto_bind_goal, auto_bind_facts;
1999-06-05, by wenzelm
auto_bind_goal, auto_bind_facts;
1999-06-05, by wenzelm
added get_st;
1999-06-05, by wenzelm
tuned;
1999-06-05, by wenzelm
varifyT': observe additional 'fixed' tfrees;
1999-06-05, by wenzelm
removed ObjectLogic.setup;
1999-06-05, by wenzelm
proper calculation;
1999-06-05, by wenzelm
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
1999-06-05, by wenzelm
fixed "...": dest_arg;
1999-06-04, by wenzelm
oops;
1999-06-04, by wenzelm
added order_le_less_trans, order_less_le_trans;
1999-06-04, by wenzelm
Calculation.thy: Setup transitivity rules for calculational proofs.
1999-06-04, by wenzelm
Support for calculational proofs.
1999-06-04, by wenzelm
added put_st;
1999-06-04, by wenzelm
added the_fact, level;
1999-06-04, by wenzelm
export multi_resolve;
1999-06-04, by wenzelm
added also, finally;
1999-06-04, by wenzelm
added 'also', 'finally' commands;
1999-06-04, by wenzelm
added COMP attribute;
1999-06-04, by wenzelm
added calculation.ML;
1999-06-04, by wenzelm
added Isar/calculation.ML;
1999-06-04, by wenzelm
fixed BUG in have_thmss: return thy';
1999-06-04, by wenzelm
added dest_main_statement;
1999-06-04, by wenzelm
print "..." variable;
1999-06-04, by wenzelm
no message "Adding axioms for datatype(s)";
1999-06-04, by wenzelm
added Group.thy;
1999-06-04, by wenzelm
added Isar_examples/Group.thy;
1999-06-04, by wenzelm
Some bits of group theory. Demonstrate calculational proofs.
1999-06-04, by wenzelm
read_term/prop_pat: do not freeze;
1999-06-02, by wenzelm
added dddot_tr;
1999-06-02, by wenzelm
added dddot_indexname;
1999-06-02, by wenzelm
"..." syntax;
1999-06-02, by wenzelm
find -print;
1999-06-02, by wenzelm
'kill' made improper;
1999-06-01, by wenzelm
improved print_state;
1999-06-01, by wenzelm
'note': Toplevel.print;
1999-06-01, by wenzelm
tuned markup;
1999-06-01, by wenzelm
broder size 3;
1999-06-01, by wenzelm
setup_goal: proper handling of non-atomic goals (include cprems into asms);
1999-05-31, by wenzelm
Isabelle manuals now also available as PDF;
1999-05-31, by wenzelm
move pdfs back into dist;
1999-05-28, by wenzelm
pdf docs;
1999-05-28, by wenzelm
separate archive for pdf docs;
1999-05-28, by wenzelm
\def\bold;
1999-05-28, by wenzelm
tuned formal comments;
1999-05-28, by wenzelm
tuned manual.bib;
1999-05-28, by wenzelm
changed {| |} verbatim syntax to {* *};
1999-05-27, by wenzelm
changed {| |} verbatim syntax to {* *} in order to simplify ProofGeneral setup;
1999-05-27, by wenzelm
improved undo / kill operations;
1999-05-27, by wenzelm
fixed corruptoin of end of file
1999-05-27, by paulson
removal of Always_StableI
1999-05-27, by paulson
replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
1999-05-27, by paulson
component_eq_subset: a neat characterization of "component"
1999-05-27, by paulson
ex/Points Isar'ized;
1999-05-26, by wenzelm
local_qed: print_result;
1999-05-26, by wenzelm
cannot_undo;
1999-05-26, by wenzelm
cannot_undo;
1999-05-26, by wenzelm
qed_block keywords;
1999-05-26, by wenzelm
local qeds: pass cond_print_result;
1999-05-26, by wenzelm
cleaned comments;
1999-05-26, by wenzelm
new theories Follows and ListOrder
1999-05-26, by paulson
formal comments (still dummy);
1999-05-25, by wenzelm
added formal comment arguments almost everywhere (still ignored);
1999-05-25, by wenzelm
renamed Comment.empty to Comment.none;
1999-05-25, by wenzelm
renamed Comment.empty to Comment.none;
1999-05-25, by wenzelm
renamed empty to none;
1999-05-25, by wenzelm
fixed cvs Id;
1999-05-25, by wenzelm
outer syntax keyword classification;
1999-05-24, by wenzelm
added keyword classification;
1999-05-24, by wenzelm
tuned print_context;
1999-05-24, by wenzelm
write_keywords generates outer syntax keyword classification in elisp;
1999-05-24, by wenzelm
outer syntax keyword classification;
1999-05-24, by wenzelm
renamed Lprg to Lift; simplified proof of Always_nonneg
1999-05-24, by paulson
int_Suc->int_Suc_int_1 avoiding confusion with the more useful Bin.int_Suc
1999-05-24, by paulson
Better simplification of (nat #0), (int (Suc 0)), etc
1999-05-24, by paulson
UN_singleton->UN_constant_eq removes clash with other UN_singleton
1999-05-24, by paulson
new rule single_leadsTo_I; stronger PSP rule
1999-05-24, by paulson
increasing makes sense only for partial orderings
1999-05-24, by paulson
generalized increasing_size to mono_increasing_o
1999-05-24, by paulson
updated for stronger version of psp
1999-05-24, by paulson
new rule single_LeadsTo_I; stronger PSP rule; PSP_stable2->PSP_Stable2
1999-05-24, by paulson
expandshort
1999-05-24, by paulson
lists are partially ordered by the prefix relation
1999-05-24, by paulson
using generic rules when possible
1999-05-24, by paulson
Theory of the "Follows" relation
1999-05-24, by paulson
Increasing makes sense only for partial orderings
1999-05-24, by paulson
generalized Increasing_size to mono_Increasing_o
1999-05-24, by paulson
tidied
1999-05-24, by paulson
renamed PSP_stable2->PSP_Stable2
1999-05-24, by paulson
now uses mono_Increasing_o
1999-05-24, by paulson
updated for stronger version of psp
1999-05-24, by paulson
Configuration for ProofGeneral of LFCS Edinburgh.
1999-05-21, by wenzelm
Configuration for David Aspinall's Isamode.
1999-05-21, by wenzelm
Miscellaneous interfaces.
1999-05-21, by wenzelm
Isamode.setup, ProofGeneral.setup;
1999-05-21, by wenzelm
Isamode and ProofGeneral configuration moved to Pure/Interface;
1999-05-21, by wenzelm
added use_thy_only;
1999-05-21, by wenzelm
added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;
1999-05-21, by wenzelm
avoid string constants;
1999-05-21, by wenzelm
qed indexed.
1999-05-21, by nipkow
typedef_proof: pass interactive flag;
1999-05-21, by wenzelm
tuned;
1999-05-21, by wenzelm
cleaned comments;
1999-05-21, by wenzelm
renamed 'begin' / 'end' to '{{' / '}}';
1999-05-21, by wenzelm
history commands;
1999-05-21, by wenzelm
tuned;
1999-05-21, by wenzelm
adapted to History changes;
1999-05-21, by wenzelm
local_qed: obtain interactive flag;
1999-05-21, by wenzelm
backup replaced by checkpoint;
1999-05-21, by wenzelm
added default_prompt;
1999-05-21, by wenzelm
optional limit;
1999-05-21, by wenzelm
improved errors;
1999-05-21, by wenzelm
updated comment
1999-05-21, by paulson
made definition more readable
1999-05-21, by paulson
preferring generic rules to specific ones...
1999-05-21, by paulson
changes to show that Lists are partially ordered by the prefix relation
1999-05-21, by paulson
deleted some vestigal theorems (use the equivalents on HOL/Ord.ML)
1999-05-21, by paulson
redid proofs to use "always" rather than "reachable" (somewhat)
1999-05-19, by paulson
new theorem Always_reachable
1999-05-19, by paulson
tuned;
1999-05-18, by wenzelm
added Locale paper
1999-05-18, by paulson
locale documentation (from Florian)
1999-05-18, by paulson
../manual.bib a new dependency
1999-05-18, by paulson
cleaned comments;
1999-05-17, by wenzelm
cleaned comments;
1999-05-17, by wenzelm
tuned;
1999-05-17, by wenzelm
cleaned comments;
1999-05-17, by wenzelm
ThyInfo.finalize_all renamed to ThyInfo.finish;
1999-05-17, by wenzelm
node_cases renamed to node_case;
1999-05-17, by wenzelm
prep_ext exported (again);
1999-05-17, by wenzelm
backup operation replaces transaction;
1999-05-17, by wenzelm
removed get_nodes;
1999-05-17, by wenzelm
remove_thy;
1999-05-17, by wenzelm
tuned arrows;
1999-05-17, by wenzelm
Arrows are no longer needed because of redesign of the
1999-05-17, by berghofe
Changed some file names.
1999-05-17, by berghofe
Added function get_preds.
1999-05-17, by berghofe
Added setup for BrowserInfo.
1999-05-17, by berghofe
usedir now recognizes additional option -P which is used to
1999-05-17, by berghofe
Changed interface of function use_dir.
1999-05-17, by berghofe
Present.begin_theory now needs an additional argument of type
1999-05-17, by berghofe
Reimplemented graph generator.
1999-05-17, by berghofe
Added some code to enable browser to display remote documents.
1999-05-17, by berghofe
new thm extend_JN; renamed extend_leadsto
1999-05-17, by paulson
"component" now an infix
1999-05-17, by paulson
indentation
1999-05-17, by paulson
tuned;
1999-05-15, by wenzelm
ad-hoc fix for bold indexes;
1999-05-12, by wenzelm
strip_quotes replaced by unenclose;
1999-05-12, by wenzelm
rearranged some modules;
1999-05-12, by wenzelm
rearranged order of modules;
1999-05-12, by wenzelm
Basic URLs.
1999-05-12, by wenzelm
added url.ML;
1999-05-12, by wenzelm
pdf setup;
1999-05-12, by wenzelm
tuned;
1999-05-12, by wenzelm
fixed msg;
1999-05-11, by wenzelm
moved scan.ML;
1999-05-11, by wenzelm
new comments, variable renaming, etc
1999-05-11, by paulson
tidied
1999-05-11, by paulson
changes for new manual.bib
1999-05-11, by paulson
make pdf;
1999-05-10, by wenzelm
tuned;
1999-05-10, by wenzelm
pdf setup;
1999-05-10, by wenzelm
cite HOLCF;
1999-05-10, by wenzelm
tuned;
1999-05-10, by wenzelm
axclass;
1999-05-10, by wenzelm
axclass;
1999-05-10, by wenzelm
pdf setup;
1999-05-10, by wenzelm
*** empty log message ***
1999-05-10, by wenzelm
*** empty log message ***
1999-05-10, by wenzelm
pdf setup;
1999-05-10, by wenzelm
fixed URLs;
1999-05-10, by wenzelm
pdf setup;
1999-05-10, by wenzelm
replaced png by pdf;
1999-05-07, by wenzelm
pdf pics;
1999-05-07, by wenzelm
tidied
1999-05-07, by paulson
tidied
1999-05-07, by paulson
new refererences for Inductive manual, but still incomplete
1999-05-07, by paulson
tuned;
1999-05-06, by wenzelm
pdf setup;
1999-05-06, by wenzelm
*** empty log message ***
1999-05-06, by wenzelm
pdf setup;
1999-05-06, by wenzelm
tuned;
1999-05-06, by wenzelm
More refs.
1999-05-06, by nipkow
Refs.
1999-05-06, by nipkow
New title page.
1999-05-06, by nipkow
tuned;
1999-05-05, by wenzelm
manual.bib;
1999-05-05, by wenzelm
no rail;
1999-05-05, by wenzelm
fixed FILES;
1999-05-05, by wenzelm
improved Makefile;
1999-05-05, by wenzelm
improved Makefile;
1999-05-05, by wenzelm
isabelle.eps;
1999-05-05, by wenzelm
improved Makefile;
1999-05-05, by wenzelm
tuned;
1999-05-05, by wenzelm
improved Makefile;
1999-05-05, by wenzelm
*** empty log message ***
1999-05-05, by wenzelm
Common part for Doc Makefiles;
1999-05-05, by wenzelm
Now uses manual.bib; some references updated
1999-05-05, by paulson
tuned rpm file names;
1999-05-05, by wenzelm
updated docs;
1999-05-05, by wenzelm
Bibtex database for documentation.
1999-05-05, by nipkow
Bibtex stuff.
1999-05-05, by nipkow
*** empty log message ***
1999-05-04, by wenzelm
HOL;
1999-05-04, by wenzelm
removed HOL.tex;
1999-05-04, by wenzelm
tuned;
1999-05-04, by wenzelm
updated;
1999-05-04, by wenzelm
HOL part moved to 'logics-HOL' manual;
1999-05-04, by wenzelm
fixed;
1999-05-04, by wenzelm
used to be part of 'logics' manual;
1999-05-04, by wenzelm
isabelle_zf image;
1999-05-04, by wenzelm
*** empty log message ***
1999-05-04, by wenzelm
Arithmetic.
1999-05-04, by nipkow
add_recdef: removed names / attributes;
1999-05-04, by wenzelm
new definitions of Co and LeadsTo
1999-05-04, by paulson
transaction: Theory.copy;
1999-05-04, by wenzelm
hide prep_ext, merge_theories;
1999-05-04, by wenzelm
oops;
1999-05-04, by wenzelm
tuned;
1999-05-04, by wenzelm
Invariant -> Always and other tidying
1999-05-04, by paulson
tuned;
1999-05-03, by wenzelm
theory loader stuff updated and improved;
1999-05-03, by wenzelm
fixed reqs?
1999-05-03, by wenzelm
improved error handling
1999-05-03, by paulson
renamed state variables
1999-05-03, by paulson
tidied
1999-05-03, by paulson
tuned;
1999-05-03, by wenzelm
prefer /bin for ./configure;
1999-05-03, by wenzelm
try chown root:root;
1999-05-03, by wenzelm
renamed 'dummy' to 'dummy_pattern' (less dangerous);
1999-05-01, by wenzelm
tuned;
1999-04-30, by wenzelm
method = meth3 (again);
1999-04-30, by wenzelm
peoper defer_recdef interface;
1999-04-30, by wenzelm
theory data: copy;
1999-04-30, by wenzelm
separated recdef / defer_recdef;
1999-04-30, by wenzelm
tuned defer_recdef interfaces;
1999-04-30, by wenzelm
comment, interest;
1999-04-30, by wenzelm
Comment.text;
1999-04-30, by wenzelm
comment sections;
1999-04-30, by wenzelm
dummy patterns;
1999-04-30, by wenzelm
added Isar/comment.ML;
1999-04-30, by wenzelm
val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term;
1999-04-30, by wenzelm
theory data: copy;
1999-04-30, by wenzelm
theory data: copy;
1999-04-30, by wenzelm
improved icons;
1999-04-30, by wenzelm
Isabelle icons;
1999-04-30, by wenzelm
patched sum_case;
1999-04-30, by wenzelm
Obsolete because JDK 1.1.x contains a class ScrollPane
1999-04-29, by berghofe
Updated to JDK 1.1.x
1999-04-29, by berghofe
Proof mods due to eta contraction during rewriting.
1999-04-29, by nipkow
Eta contraction is now performed all the time during rewriting.
1999-04-29, by nipkow
currently disabled;
1999-04-29, by wenzelm
*** empty log message ***
1999-04-29, by wenzelm
made many specification operators infix
1999-04-29, by paulson
eliminated theory UNITY/Traces
1999-04-28, by paulson
improper simp methods;
1999-04-27, by wenzelm
tuned;
1999-04-27, by wenzelm
fold / unfold methods;
1999-04-27, by wenzelm
tuned;
1999-04-27, by wenzelm
no Toplevel.print for by, ., ..;
1999-04-27, by wenzelm
improved print_state;
1999-04-27, by wenzelm
verbose flag;
1999-04-27, by wenzelm
use_thy_only made pervasive;
1999-04-27, by wenzelm
added Isar_examples/NatSum.thy;
1999-04-27, by wenzelm
Old stuff.
1999-04-27, by nipkow
proper quiet_mode;
1999-04-27, by wenzelm
adapted add_inductive, add_record;
1999-04-27, by wenzelm
adapted add_inductive;
1999-04-27, by wenzelm
intrs attributes;
1999-04-27, by wenzelm
proper quiet_mode;
1999-04-27, by wenzelm
iff_add_global (from simpdata.ML);
1999-04-27, by wenzelm
support forward chaining;
1999-04-27, by wenzelm
tuned;
1999-04-27, by wenzelm
added Isar_examples/Cantor.ML;
1999-04-27, by wenzelm
hol_setup, simpdata_setup;
1999-04-27, by wenzelm
"iff" attribute;
1999-04-27, by wenzelm
hol_setup;
1999-04-27, by wenzelm
"!" made keyword;
1999-04-27, by wenzelm
opt_thm_name: name optional;
1999-04-27, by wenzelm
added oooo;
1999-04-27, by wenzelm
fixed a bug many years old in rule plusEC
1999-04-26, by paulson
tuned msgs;
1999-04-26, by wenzelm
tuned;
1999-04-23, by wenzelm
tuned;
1999-04-23, by wenzelm
elaborated;
1999-04-23, by wenzelm
tuned;
1999-04-23, by wenzelm
tuned antiquotations;
1999-04-23, by wenzelm
improved 'single' method;
1999-04-23, by wenzelm
less
more
|
(0)
-3000
-1000
-960
+960
+1000
+3000
+10000
+30000
tip