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.
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
less
more
|
(0)
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip