working version with co-guarantees-leadsto results

tuned;

tuned;

qed "";

tuned print_result;

improved cycle error;

Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or RealAbs. RealAbs proofs have been highly streamlined. A couple of RealPow proofs use #1, #2, etc.

sep1 -> sep

The restrict_to_left rule fixes some bugs

Sets new component "restrict_to_left"

tidied; added lemma restrict_to_left

Restructured lin.arith.package and fixed a proof in RComplete.

Restructured lin.arith.package.

thms_containing: single writeln;

tuned pretty_thms;

added thms_containing;

qed "";

proper theory setup for Real/ex/BinEx;

tuned;

improved output;

added 'insert' method (again);

ml_store_thm: no warning for "";

present results;

merged in lost update;

Mod because of new solver interface.

?

Solvers are now named and stamped.

fixed unfold of facts;

accomodate refined facts handling;

accomodate refined facts handling; tuned;

Main;

Thm.no_prems;

tuned;

added some ~= rules;

removed "case" thm;

setup for refined facts handling; Method.bang_sectioned_args / Args.bang_facts;

setup for refined facts handling; Method.bang_sectioned_args / Args.bang_facts; eliminated asm_simp; tuned improper methods;

export prems_of;

setup_goal: do not insert assumptions;

setup for refined facts handling; tuned insert_facts, assumption, (un)fold; insert_tac: no rotate_tac, order was OK in the first place; added ctxt_args, bang_sectioned_args; added assm_tac;

differ: compare actual props only (hyps may changed due to trivial steps involving assumptions);

added bang_facts;

Added comments.

Now distinguishes discrete from non-distrete types.

moved inf_of(?) to hologic.

Integ/bin_simprocs.ML now loaded in Integ/Bin.ML

ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML

new proof of drop_prog_correct for new definition of project_act

project_act no longer has a special case to allow identity actions

fixed SOUNDNESS BUG concerning the map from terms like ?f x y to SVC variables

Fixed bug in add_primrec which caused non-informative error message.

renamed Always_Int to Always_Int_I

new theorem mono_Follows_apply

new theorem Always_INT_distrib; therefore renamed Always_Int to Always_Int_I

working Safety proof for the system at last

now uses Pattern.aeconv, not aconv, to test equality between the terms abstracted over; otherwise it is incomplete. Other changes are cosmetic

new rule PLam_ensures

working snapshot

new theorem image_image_eq_UN

The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar) (by Gertrud Bauer, TU Munich);

added no_prems;

minor change to smp_tac

fixed url;

AddXDs [bspec];

tuned;

AddXIs [disjI1, disjI2];

removed obsolete comment;

lemma less_add;

(un)fold: ignore facts;

more rational theorem names (?)

tidied

more rational theorem names (?)

ensures_tac now handles leadsTo as well as LeadsTo

new theorem single_Diff_lessThan

now uses the identity function

simplification of relations involving 0, Suc and natural-number numerals

generalized the theorem zless_zero_nat to zless_nat_eq_int_zless, and reorganized

generalized the theorem bin_add_BIT_Min to bin_add_Min_right

moved identity theorems to Fun.ML

comments

images and preimages of the identity function

new example HOL/UNITY/TimerArray

rule option;

\indexisarmeth: "Methods";

tuned (then_)apply;

url;

\url;

induct method: rule option;

Method.refine_no_facts;

read_def_termT: dummyT;

then_tac = refine;

read_typ/term: context_of;

tuned;

added context_of;

logtypes: pretend "dummy" is one;

isatool expandshort;

expandshort usage: forward_tac;

strengthened card_seteq

added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD

added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc

added theorems le_maxI1 and le_maxI2, also in claset

added theorem dvd_reduce

*** empty log message ***

added ftac, eatac, datac, fatac

added smp_tac

added;

isabelle-pdfdocs;

close_block: removed ProofContext.transfer_used_names;

removed thms_closure (unused); removed transfer_used_names; fix: do not declare unconstrained vars;

removed thms_closure (unused);

added README;

tuned;

working snapshot

goal_nonempty: Ex goal for new-style version;

replaced ?? by ?;

eliminated Syntax.binding; put_thms: ignore ""; update_binds_env: Envir.norm_term ensures proper type instantiation;

deactivated ProofContext.transfer_used_names; eliminated PureThy.default_name ("" not stored);

removed text vars;

PureThy.have_thmss: "" replaces None;

Library.equal_lists;

removed Syntax.binding;

removed "_BIND" translation;

removed binding;

removed "_BIND" syntax;

eliminated default_name (thms no longer stored for name "");

ProtoPure: fake empty scope;

equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool;

handle Bind!!

updated;

added \indexisarvar;

removed \VVar;

usage: tell OPTIONS;

added welcome;

usage: tell ISABELLE_USEDIR_OPTIONS;

tuned;

usage: tell current OPTIONS value;

updated;

fixed usepackage;

permuted index;

\PROP;

no_qed; bind_thms;

no_qed;

"this";

tuned;

added bind_thms;

tuned K;

tuned;

from hyp;

added no_qed;

new theorem fun_upd_upd

new SVC url

renamed NatSum to Summation;

tidied;

AddXDs [bspec];

added with_path;

terminal method: always involve finish;

with_path;

renamed improper method 'clarsimp' to 'clarsimp_tac';

added MultisetOrder.thy;

Isar_examples/MultisetOrder.thy;

tuned;

"this";

Wellfoundedness proof for the multiset order (preliminary version).

fix: vars;

removed "*" method combinator;

observe show_types;

bind_thms;

bind_thm "case";

*: no quotes;

Method.insert_tac; Method.multi_resolves; contradiction: made faithful; tuned comments;

Method.insert_tac;

Method.insert_tac; tuned comments;

bind_thm;

added bind_thms, store_thms;

structures Vartab / Termtab (instances of TableFun);

tuned; renamed same_tac to insert_tac; improved assumption; removed Repeat; immediate_proof: assumption;

any_props: improved error; removed "*" method combinator;

fix: common constraints; cond_print_calc: Proof.pretty_thm;

Thm.def_name;

replaced IsarCmd.kill_theory by Toplevel.kill; fix: common constraints; removed "*" keyword;

calculation: thm list; filter differ;

removed kill_theory; print_thms: use Proof.pretty_thms;

removed the_fact; added pretty_thms; fix: common constraints; renamed "facts" to "this"; print_state: tuned "Using facts";

fix: common constraints;

added store/bind_thms;

added theorems; improved files;

added theorems; begin_theory: implicit files;

isar: avoid verbose goal responses;

structure Termtab;

smart_store_thms;

PureThy.smart_store_thms;

tidied some proofs

tidied

tidied

new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration for the overloading of <, while .ML file gets proofs about renaming constants

changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <

proper calculation / induction;

tuned;

OF: "_" as argument;

clean: include HOL-Real-ex;

auto: CHANGED;

make it actually RUN the real examples

new directory HOL/Real/ex of real examples

'iff' attribute;

'arith' method;

'_' theorem; back: only latest command;

tuned;

new results for localTo

a new theorem

tuned;

added MutilatedCheckerboard;

added Isar_examples/MutilatedCheckerboard.thy;

The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;

tuned;

thm "_" = asm_rl;

tidied

use of bij, new theorems, etc.

the bij predicate forced renaming of a variable bij

tidied, allowing pattern-matching in defs of prat_add and prat_mult

tidied, allowing pattern-matching in defs of zadd and zmult

the bij predicate (at last)

better timing information;

oops;

*** empty log message ***

tuned;

iff_attrib_setup;

improved back, help;

print_help;

back: recur flag;

a bit further with property (1)

changed "guar" back to "guarantees" (sorry) and FIXED ITS PRECEDENCE

new destruction rules

new laws; changed "guar" back to "guarantees" (sorry)

changed "guar" back to "guarantees" (sorry)

more Join rules including AC-rules

extra syntax for JN, making it more like UN

a little tidying; also FIXED BAD TYPE in INTER1, UNION1

proper bootstrap of HOL theory and packages;

expand_classes renamed to intro_classes;

proper bootstrap of IFOL/FOL theories and packages;

proper setup of GlobalClaset data;

improved msg;

fixed arity;

expand_classes renamed to intro_classes;

TPHOLs99;

Removed "Adding axioms ..." message.

hide private parts;

another snapshot

arguably clearer definition of the inductive case of leads-to. No proofs had to be changed...

tidied

new guarantees laws; also better natural deduction style for old ones

renamed some theorems; also better natural deduction style for old ones

project constants

many "project" laws

new guarantees laws; also better natural deduction style for old ones

split_paired_Eps and lemmas

new theorem inv_f_eq

%dir;

tuned;

draft release;

Real/Real.thy main entry point;

isar: no_pos flag;

fixed add_sect etc.;

??thesis: include params;

print_mode activated again;

fixed intro_elim_tac;

record_simproc;

tuned;

record_simproc;

Some changes in sections about Sum and Nat.

simplifier flex heads.

Now rewrite rules with flexible heads are allowed.

isatool expandshort;

tuned;

Moved sum_case to theory HOL/Datatype.

tuned;

Corrected two busg in the simplifier.

\indexisarreg;

\VVar;

checkpoint;

tuned; fixed HOL-Real;

real numerals;

added HOL-Real; made relocatable;

echo ML_PLATFORM;

activate example;

delcongs [if_weak_cong];

print_context;

eliminated HOL-AxClasses target;

intro (no +);

mucke -res;

if_svc_enabled;

AxClasses, Isar_examples;

intro/elim: REPEAT1;

new theories RealBin, RealInt, RealPow

* HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with HOL/List;

quite a lot of tuning and cleanup;

sysman: Stefan Berghofer;

more;

Mucke, Einhoven;

quite a lot of tuning an cleanup;

sum_case_Inl and sum_case_Inr are now defined in Datatype.ML.

Moved sum_case stuff from Sum to Datatype.

real literals using binary arithmetic

new entriues.

updated

disabled print_mode (tmp);

lookup_theory;

defer_recdef

removed needless comments

removed all unnecessary code

now with abstraction code previously in HOL/Tools/svc_funcs.ML

documented svc_tac

finished theories;

renamed 'some_rule' to 'rule';

tuned;

removed fixnumerals (for the time being);

tuned Goal syntax;

improved messages;

really removed -m option;

removed -m option;

usedir: removed -m option;

Method.modifier; fixed 'only:';

Method.modifier;

assume: multiple args;

warn_vars; tuned strings_of_context; assume(_i): multiple args;

assume/presume: and_list1;

sectioned_args etc.: more general modifier;

deps: include 'really' flag;

isa_action: don't lock pretend_used files;

proper writeln of begin_state;

(*no fix_shyps*);

tuned messages;

from Konrad: support for schematic definitions

sum_case renamed to basic_sum_case;

Removed rbeta.

tuned messages;

tuned;

Renamed sum_case to basic_sum_case.

Eliminated some infixes.

Eliminated some infixes.

Renamed sum_case to basic_sum_case and removed translations for sum_case to avoid conflicts with the constant sum_case introduced in Datatype.thy.

tuned;

replaced 'ProofGeneral' by 'Proof General';

Modified section about generation of theory browsing information. Documented new -P option.

new version from Konrad with "lazy" (deferred) definitons

tidied some proofs

new primitive rule permute_prems to underlie defer_tac and rotate_prems

freeze_thaw does nothing if no variables

Added take_all and drop_all to simpset.

eliminated HOL_quantifiers (replaced by "HOL" print mode);

may_load_file; use_thy etc.: warn_finished; added begin_update_theory; added quiet_update_thy;

ThyInfo.may_load_file;

begin_update_theory;

PASS(_MODE): works better without space (why?);

removed HOL_quantifiers;

HOL_quantifiers;

replaced HOL_quantifiers flag by "HOL" print mode; simplified HOL basic syntax (more orthogonal);

turned SVC_Oracle into a new-style theory in order to get automatic handling of its additional dependency on Tools/svc_funcs.ML;

Better handling of path for remote theory browsing information.

Goals.reset_goals;

reset_goals;

intro+;

remove tmp files;

tuned;

renamed 'single' to 'some_rule'; added 'intro', 'elim';

renamed Cons to Consq in order to avoid clash with List.Cons;

Tuned some comments.

Path for remote theory browsing information is now stored in referece variable rpath.

-m option;

replaced "op #" by "Cons";

'a list: Nil, Cons;

tuned msg;

disable_pr, enable_pr;

deleted obsolete assignment

restored a high precedence to unary minus

inserted Id: lines

new theory Real/Hyperreal/HyperDef and file fuf.ML

forgot to write back adaption of onlysimps

tuned;

tuned;

exchanged finish_tac and unsafe_finish_tac (the more important one) in simpset basic_gen_simp_tac now takes a looper as _explicit_ argument removed superfluous argument of solve_all_tac corrected safe_asm_full_simp_tac: now also with mutual simplification of prems

re-added refl in safe_solver

removed warn_theory_style;

fixed thy_only;

tuned prompts;

isamode;

user infaces: tuned, added ProofGeneral;

bib;

-m option;

Tuned.

Removed * reset HOL_quantifiers by default, i.e. quantifiers are printed as ALL/EX rather than !/?;

* set HOL_quantifiers by default, i.e. quantifiers are printed as !/? rather than ALL/EX;

added asym rule;

tuned print_state;

tuned strings_of_context; fix: check identifier;

pr / no_pr: maintain Toplevel.quiet;

tuned print_state; quiet flag;

append user rules;

theory loader actions;

made SML happy;

tuned;

proper ProofGeneral/isa setup;

simplified ML handling;

added pretend_use; simplified ML handling; loaded_files: include thy; perform Remove *before* actual deletion; perform: made bullet proof;

simplified handling of ML file; improved master info;

the whole file is now loaded only if SVC is enabled

re-organization of theorems from Alloc and PPROD, partly into new theory Lift_prog

svc_enabled is now declared as a function

new theory UNITY/Lift_prog

External reasoning tools;

no longer gives a default value to SVC_MACHINE

extra comment

now catches exn THEORY and prints an error message

some hard propositional examples

new theory ex/svc_test.thy

removed obsolete addsimps update_defs;

record_simproc for sel-upd (by Sebastian Nanz); removed record_splitter by default;

change_simpset_of;

local goals: after_qed;

tuned;

added isabelle-sys, proofgeneral;

improved \NOTE; added \BYY;

tuned; added sect, subsect, subsubsect;

improved interest;

tuned;

tuned attdx, methdx; added descr env;

fixed {};

tuned; much more material;

Sara Kalvala: moving the <<...>> notation from LK to Sequents

new examples file for SVC

biconditionals and the natural numbers

added realT

biconditionals and the natural numbers

new examples file for SVC

new chapter on Sequents

\underscoreoff needed because of \underscoreon in previous file

new variables for SVC

SVC

fixed Blast_Data;

blast method: optional depth argument;

export cla_meth(');

tuned;

tuned outer syntax;

handle LIST _;

cat_lines;

provide String structure;

removed obsolete concat;

String.isPrefix

long-overdue updating

new files for the SVC link-up

the SVC oracle theory

the SVC link-up

new files for the SVC link-up

even more stuff;

oracle: '=';

added \text;

Isabelle/Isar macros;

hacking the rail package;

added update_thy_only; moved update_thy;

more;

more stuff;

renamed 'same' to '-';

eliminated METHOD0 in favour of same_tac;

'arith' proof method;

added erule; renamed same to -;

export sysify_path;

split_diff and remove_diff_ss

added parentheses to cope with a possible reduction of the precedence of unary minus

ML_HOME=$ISABELLE_HOME/../smlnj/bin;

HOL-Real target now builds an actual image;

added pretty_setmargin;

congruence rule for |-, etc.

renamed ...thm_pack... to ...pack...

removed the unused SeqVar option

sequents require higher bounds

more examples are working

adding missing declarations for the <<...>> notation

congruence rule for |-

simplifier and improved classical reasoner

mkdir contrib;