isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -1000 -120 +120 +1000 +3000 +10000 +30000 tip

added token_translation interface;
1997-02-28, by wenzelm
added add_tokentrfuns;
1997-02-28, by wenzelm
added Syntax/token_trans.ML;
1997-02-28, by wenzelm
added token_trans.ML;
1997-02-28, by wenzelm
Slightly more robust proof
1997-02-28, by paulson
dup_intr & dup_elim no longer call standard -- this
1997-02-28, by paulson
rule_by_tactic no longer standardizes its result
1997-02-28, by paulson
Addition of de Bruijn formulae
1997-02-28, by paulson
tuned comment;
1997-02-27, by wenzelm
tuned comments;
1997-02-27, by wenzelm
added proper subset symbols syntax;
1997-02-25, by wenzelm
minor changes due to primrec defintions for +,-,*
1997-02-25, by pusch
minor changes due to new primrec definitions for +,-,*
1997-02-25, by pusch
definitions of +,-,* replaced by primrec definitions
1997-02-25, by pusch
function nat_add_primrec added to allow primrec definitions over nat
1997-02-25, by pusch
removed explicit_domains/, which is now covered by ex/
1997-02-24, by oheimb
added "_" syntax for dummyT;
1997-02-24, by wenzelm
declared the dummy type;
1997-02-21, by wenzelm
replaced natural by subset;
1997-02-21, by wenzelm
tuned symbolic [|_|] syntax;
1997-02-21, by wenzelm
tuned some chars;
1997-02-21, by wenzelm
More robust proof (?)
1997-02-21, by paulson
Replaced "flat" by the Basis Library function List.concat
1997-02-21, by paulson
Introduction of rotate_rule
1997-02-21, by paulson
removed empty line (which broke xfedor);
1997-02-21, by wenzelm
don't hack, use xfed or xfedor;
1997-02-21, by wenzelm
fixed Id comment;
1997-02-21, by wenzelm
makedist -- make Isabelle distribution.
1997-02-20, by wenzelm
tuned URL;
1997-02-20, by wenzelm
added index info;
1997-02-20, by wenzelm
index info;
1997-02-20, by wenzelm
added dist;
1997-02-20, by wenzelm
some administrative tools for the Isabelle;
1997-02-20, by wenzelm
made a bit more robust for 'make dist';
1997-02-20, by wenzelm
rail output;
1997-02-20, by wenzelm
fixed rail.sty dep;
1997-02-20, by wenzelm
added this file;
1997-02-20, by wenzelm
rail output;
1997-02-20, by wenzelm
made a bit more robust;
1997-02-20, by wenzelm
manual steps comment;
1997-02-17, by wenzelm
*** empty log message ***
1997-02-17, by wenzelm
described changes for HOLCF-Version without rules and arities
1997-02-17, by slotosch
file moved;
1997-02-17, by wenzelm
file moved here;
1997-02-17, by wenzelm
configure - adapt Isabelle distribution to system environment
1997-02-17, by wenzelm
improved description of recent changes
1997-02-17, by oheimb
reflecting recent changes of the simplifier
1997-02-17, by slotosch
corrected type of plift
1997-02-17, by oheimb
reflecting recent changes of the simplifier
1997-02-17, by oheimb
mk_rews: automatically includes strip_shyps, zero_var_indexes;
1997-02-17, by wenzelm
New file for theorems of Porder0
1997-02-17, by slotosch
tuned comments;
1997-02-17, by wenzelm
Examples are adopted to the changes from HOLCF.
1997-02-17, by slotosch
using types one = unit lift and translations causes troubles between
1997-02-17, by slotosch
Changes of HOLCF from Oscar Slotosch:
1997-02-17, by slotosch
*** empty log message ***
1997-02-15, by oheimb
reflecting my recent changes of the classical reasoner
1997-02-15, by oheimb
reflecting my recent changes of the simplifier and classical reasoner
1997-02-15, by oheimb
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
1997-02-15, by oheimb
cosmetic
1997-02-15, by oheimb
updated mini_ss
1997-02-15, by oheimb
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
1997-02-15, by oheimb
corrected minor mistakes
1997-02-15, by oheimb
description of safe vs. unsafe wrapper and the functions involved
1997-02-15, by oheimb
moved THEN_MAYBE to Pure/tctical.ML
1997-02-15, by oheimb
added deleqcongs, richer rep_ss
1997-02-15, by oheimb
description of del(eq)congs, safe and unsafe solver
1997-02-15, by oheimb
added THEN_MAYBE and THEN_MAYBE'
1997-02-15, by oheimb
added del_congs
1997-02-15, by oheimb
Some lemmas changed to valuesd
1997-02-14, by narasche
fixed comment;
1997-02-14, by wenzelm
improved interface options;
1997-02-14, by wenzelm
semi fix of piping-quit peoblem (should work on systems with *real* sh);
1997-02-14, by wenzelm
globally unset ENV, BASH_ENV;
1997-02-14, by wenzelm
Made troublesome simplifier warning dependent on trace_simp.
1997-02-14, by nipkow
Modified and shortened adm_disj lemmas.
1997-02-14, by nipkow
Deleted a useless definition
1997-02-14, by paulson
Added optimization: do nothing for empty list
1997-02-14, by paulson
A bit more pattern-matching in eta_contract
1997-02-14, by paulson
Tidying and a corrected comment
1997-02-14, by paulson
Added a new challenge problem
1997-02-14, by paulson
Updated documentation of IFOL_ss
1997-02-14, by paulson
Documented thin_tac
1997-02-14, by paulson
Strengthened warnings concerning topthm(), etc.
1997-02-14, by paulson
Updated a reference
1997-02-14, by paulson
New class "order" and accompanying changes.
1997-02-12, by nipkow
New class "order" and accompanying changes.
1997-02-12, by nipkow
TFL: missing -q option!
1997-02-12, by wenzelm
tuned names: partial order, linear order;
1997-02-12, by wenzelm
tuned startup;
1997-02-10, by wenzelm
fixed comment;
1997-02-10, by wenzelm
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
1997-02-10, by paulson
Renamed structure Int (intuitionistic prover) to IntPr
1997-02-10, by paulson
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
1997-02-10, by paulson
removed ISABELLE_INTERFACE_OPTIONS;
1997-02-07, by wenzelm
tuned;
1997-02-07, by wenzelm
tuned;
1997-02-07, by wenzelm
Modified proofs due to added triv_forall_equality.
1997-02-07, by nipkow
Modified proofs because of added "triv_forall_equality".
1997-02-07, by nipkow
Added "triv_forall_equality" to HOL_ss.
1997-02-07, by nipkow
functionality added to getsettings;
1997-02-06, by wenzelm
removed getplatform, ISABELLE_OUTPUT_DIR;
1997-02-06, by wenzelm
removed getplatform, ISABELLE_OUTPUT_DIR;
1997-02-06, by wenzelm
removed getplatform;
1997-02-06, by wenzelm
integrated getplatform stuff;
1997-02-06, by wenzelm
now falls back on ucat instead of cat;
1997-02-06, by wenzelm
improved usage msg;
1997-02-06, by wenzelm
added eq_sort (will move to sorts.ML eventually);
1997-02-06, by wenzelm
adapted to new Syntax.read_typ;
1997-02-06, by wenzelm
adapted read_typ, simple_read_typ;
1997-02-06, by wenzelm
improved comments;
1997-02-06, by wenzelm
added string_of_vname' (treats neg. index as free);
1997-02-06, by wenzelm
cd made readably again;
1997-02-06, by wenzelm
tuned;
1997-02-05, by wenzelm
Gradual switching to Basis Library functions nth, drop, etc.
1997-02-04, by paulson
now uses tee -i instead of perl;
1997-02-04, by wenzelm
now uses ISABELLE_INSTALLFONTS;
1997-02-04, by wenzelm
added ISABELLE_INSTALLFONTS;
1997-02-04, by wenzelm
Declaration of ccontr (classical contradiction) for HOL compatibility
1997-01-31, by paulson
Correction to Problem 24
1997-01-31, by paulson