isabelle: Graph

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

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