Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -3000 -1000 -300 -100 -64 +64 +100 +300 +1000 +3000 +10000 +30000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tue, 30 Sep 1997 17:32:33 +0200 Removed "browse.tex".
changeset
berghofe [Tue, 30 Sep 1997 17:32:33 +0200] rev 3754
Removed "browse.tex".
Tue, 30 Sep 1997 17:31:19 +0200 Added section describing the theory browser.
changeset
berghofe [Tue, 30 Sep 1997 17:31:19 +0200] rev 3753
Added section describing the theory browser.
Tue, 30 Sep 1997 17:29:32 +0200 Updated usage information for tool "usedir".
changeset
berghofe [Tue, 30 Sep 1997 17:29:32 +0200] rev 3752
Updated usage information for tool "usedir".
Tue, 30 Sep 1997 17:28:54 +0200 Theory browser stuff has been moved to "present.tex".
changeset
berghofe [Tue, 30 Sep 1997 17:28:54 +0200] rev 3751
Theory browser stuff has been moved to "present.tex".
Tue, 30 Sep 1997 16:19:27 +0200 obsolete;
changeset
wenzelm [Tue, 30 Sep 1997 16:19:27 +0200] rev 3750
obsolete;
Tue, 30 Sep 1997 16:12:38 +0200 ISABELLE_USEDIR_OPTIONS="-i true"
changeset
wenzelm [Tue, 30 Sep 1997 16:12:38 +0200] rev 3749
ISABELLE_USEDIR_OPTIONS="-i true"
Tue, 30 Sep 1997 12:53:54 +0200 Changed html data directory and names of graph files.
changeset
berghofe [Tue, 30 Sep 1997 12:53:54 +0200] rev 3748
Changed html data directory and names of graph files.
Tue, 30 Sep 1997 12:52:15 +0200 There is now one single option -i for generating theory browsing
changeset
berghofe [Tue, 30 Sep 1997 12:52:15 +0200] rev 3747
There is now one single option -i for generating theory browsing information instead of the two options -h and -g .
Tue, 30 Sep 1997 12:49:16 +0200 Modified some links.
changeset
berghofe [Tue, 30 Sep 1997 12:49:16 +0200] rev 3746
Modified some links.
Tue, 30 Sep 1997 11:03:55 +0200 Client, Server certificates now sent using the separate Certificate rule,
changeset
paulson [Tue, 30 Sep 1997 11:03:55 +0200] rev 3745
Client, Server certificates now sent using the separate Certificate rule, simplifying ServerHello and ClientKeyExch. Resumption no longer needs its own version of ServerHello. Proofs run nearly three minutes faster.
Mon, 29 Sep 1997 15:39:28 +0200 tuned;
changeset
wenzelm [Mon, 29 Sep 1997 15:39:28 +0200] rev 3744
tuned;
Mon, 29 Sep 1997 15:16:22 +0200 superficial;
changeset
wenzelm [Mon, 29 Sep 1997 15:16:22 +0200] rev 3743
superficial;
Mon, 29 Sep 1997 15:11:27 +0200 obsolete;
changeset
wenzelm [Mon, 29 Sep 1997 15:11:27 +0200] rev 3742
obsolete;
Mon, 29 Sep 1997 15:08:47 +0200 margin 76 (2nd try :-);
changeset
wenzelm [Mon, 29 Sep 1997 15:08:47 +0200] rev 3741
margin 76 (2nd try :-);
Mon, 29 Sep 1997 14:12:02 +0200 fixed href to html library;
changeset
wenzelm [Mon, 29 Sep 1997 14:12:02 +0200] rev 3740
fixed href to html library;
Mon, 29 Sep 1997 14:11:18 +0200 improved warning;
changeset
wenzelm [Mon, 29 Sep 1997 14:11:18 +0200] rev 3739
improved warning;
Mon, 29 Sep 1997 14:10:52 +0200 default margin 76 (to accomodate warning and error default output);
changeset
wenzelm [Mon, 29 Sep 1997 14:10:52 +0200] rev 3738
default margin 76 (to accomodate warning and error default output);
Mon, 29 Sep 1997 12:13:43 +0200 Step_tac -> Safe_tac
changeset
paulson [Mon, 29 Sep 1997 12:13:43 +0200] rev 3737
Step_tac -> Safe_tac
Mon, 29 Sep 1997 11:56:04 +0200 Much tidying including step_tac -> clarify_tac or safe_tac; sometimes
changeset
paulson [Mon, 29 Sep 1997 11:56:04 +0200] rev 3736
Much tidying including step_tac -> clarify_tac or safe_tac; sometimes used qed_spec_mp
Mon, 29 Sep 1997 11:52:25 +0200 Step_tac -> Safe_tac
changeset
paulson [Mon, 29 Sep 1997 11:52:25 +0200] rev 3735
Step_tac -> Safe_tac
Mon, 29 Sep 1997 11:51:52 +0200 Much tidying including "qed" instead of result(), and even qed_spec_mp,
changeset
paulson [Mon, 29 Sep 1997 11:51:52 +0200] rev 3734
Much tidying including "qed" instead of result(), and even qed_spec_mp, and Safe_tac instead of step_tac
Mon, 29 Sep 1997 11:51:09 +0200 Previously loaded the WRONG THEORY, ignoring Confluence...
changeset
paulson [Mon, 29 Sep 1997 11:51:09 +0200] rev 3733
Previously loaded the WRONG THEORY, ignoring Confluence...
Mon, 29 Sep 1997 11:49:33 +0200 Now using qed_spec_mp
changeset
paulson [Mon, 29 Sep 1997 11:49:33 +0200] rev 3732
Now using qed_spec_mp
Mon, 29 Sep 1997 11:48:48 +0200 result() -> qed; Step_tac -> Safe_tac
changeset
paulson [Mon, 29 Sep 1997 11:48:48 +0200] rev 3731
result() -> qed; Step_tac -> Safe_tac
Mon, 29 Sep 1997 11:47:01 +0200 Step_tac -> Safe_tac
changeset
paulson [Mon, 29 Sep 1997 11:47:01 +0200] rev 3730
Step_tac -> Safe_tac
Mon, 29 Sep 1997 11:46:33 +0200 Renamed XA, XB to PA, PB and removed the certificate from Client Verify
changeset
paulson [Mon, 29 Sep 1997 11:46:33 +0200] rev 3729
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
Mon, 29 Sep 1997 11:45:52 +0200 Default simpset tactics now dereference "simpset"
changeset
paulson [Mon, 29 Sep 1997 11:45:52 +0200] rev 3728
Default simpset tactics now dereference "simpset" only when given the proof state
Mon, 29 Sep 1997 11:44:56 +0200 Added Safe_tac; all other default claset tactics now dereference "claset"
changeset
paulson [Mon, 29 Sep 1997 11:44:56 +0200] rev 3727
Added Safe_tac; all other default claset tactics now dereference "claset" only when given the proof state
Mon, 29 Sep 1997 11:42:15 +0200 fast_tac HOL_cs -> Fast_tac, etc.
changeset
paulson [Mon, 29 Sep 1997 11:42:15 +0200] rev 3726
fast_tac HOL_cs -> Fast_tac, etc.
Mon, 29 Sep 1997 11:40:03 +0200 result() -> qed
changeset
paulson [Mon, 29 Sep 1997 11:40:03 +0200] rev 3725
result() -> qed
Mon, 29 Sep 1997 11:37:02 +0200 Step_tac -> Safe_tac
changeset
paulson [Mon, 29 Sep 1997 11:37:02 +0200] rev 3724
Step_tac -> Safe_tac
Mon, 29 Sep 1997 11:36:44 +0200 Tidied proof of r_comp_rtrancl_eq
changeset
paulson [Mon, 29 Sep 1997 11:36:44 +0200] rev 3723
Tidied proof of r_comp_rtrancl_eq
Mon, 29 Sep 1997 11:32:25 +0200 qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
changeset
paulson [Mon, 29 Sep 1997 11:32:25 +0200] rev 3722
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
Mon, 29 Sep 1997 11:31:56 +0200 Step_tac -> Safe_tac
changeset
paulson [Mon, 29 Sep 1997 11:31:56 +0200] rev 3721
Step_tac -> Safe_tac
Mon, 29 Sep 1997 11:31:13 +0200 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
changeset
paulson [Mon, 29 Sep 1997 11:31:13 +0200] rev 3720
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
Mon, 29 Sep 1997 11:28:23 +0200 Safe_tac; qed_spec_mp in FOL
changeset
paulson [Mon, 29 Sep 1997 11:28:23 +0200] rev 3719
Safe_tac; qed_spec_mp in FOL
Fri, 26 Sep 1997 10:21:14 +0200 Minor tidying to use Clarify_tac, etc.
changeset
paulson [Fri, 26 Sep 1997 10:21:14 +0200] rev 3718
Minor tidying to use Clarify_tac, etc.
Fri, 26 Sep 1997 10:12:04 +0200 eliminated rules;
changeset
wenzelm [Fri, 26 Sep 1997 10:12:04 +0200] rev 3717
eliminated rules; tuned;
Thu, 25 Sep 1997 13:25:50 +0200 Clarify_tac and some textual improvements
changeset
paulson [Thu, 25 Sep 1997 13:25:50 +0200] rev 3716
Clarify_tac and some textual improvements
Thu, 25 Sep 1997 13:23:41 +0200 Clarify_tac; general reorganization
changeset
paulson [Thu, 25 Sep 1997 13:23:41 +0200] rev 3715
Clarify_tac; general reorganization
Thu, 25 Sep 1997 12:32:14 +0200 Deleted obsolete version of clarify_tac
changeset
paulson [Thu, 25 Sep 1997 12:32:14 +0200] rev 3714
Deleted obsolete version of clarify_tac
Thu, 25 Sep 1997 12:25:29 +0200 Deleted the unused list_mk_disj
changeset
paulson [Thu, 25 Sep 1997 12:25:29 +0200] rev 3713
Deleted the unused list_mk_disj
Thu, 25 Sep 1997 12:24:53 +0200 Deleted the unused gtake and recoded enumerate to use foldl
changeset
paulson [Thu, 25 Sep 1997 12:24:53 +0200] rev 3712
Deleted the unused gtake and recoded enumerate to use foldl
Thu, 25 Sep 1997 12:20:24 +0200 Deleted an obsolete step in TrustServerFinished
changeset
paulson [Thu, 25 Sep 1997 12:20:24 +0200] rev 3711
Deleted an obsolete step in TrustServerFinished
Thu, 25 Sep 1997 12:19:41 +0200 Deleted obsolete axioms inj_serverK and isSym_serverK
changeset
paulson [Thu, 25 Sep 1997 12:19:41 +0200] rev 3710
Deleted obsolete axioms inj_serverK and isSym_serverK
Thu, 25 Sep 1997 12:14:41 +0200 Tidied proofs, using Clarify_tac
changeset
paulson [Thu, 25 Sep 1997 12:14:41 +0200] rev 3709
Tidied proofs, using Clarify_tac
Thu, 25 Sep 1997 12:13:18 +0200 Changed some proofs to use Clarify_tac
changeset
paulson [Thu, 25 Sep 1997 12:13:18 +0200] rev 3708
Changed some proofs to use Clarify_tac
Thu, 25 Sep 1997 12:10:07 +0200 Prints warnings using the "warning" function instead of "writeln"
changeset
paulson [Thu, 25 Sep 1997 12:10:07 +0200] rev 3707
Prints warnings using the "warning" function instead of "writeln"
Thu, 25 Sep 1997 12:09:41 +0200 Generalized and exported biresolution_from_nets_tac to allow the declaration
changeset
paulson [Thu, 25 Sep 1997 12:09:41 +0200] rev 3706
Generalized and exported biresolution_from_nets_tac to allow the declaration of Clarify_tac
Thu, 25 Sep 1997 12:08:08 +0200 Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
changeset
paulson [Thu, 25 Sep 1997 12:08:08 +0200] rev 3705
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
Wed, 24 Sep 1997 12:27:53 +0200 sessionK now indexed by nat instead of bool.
changeset
paulson [Wed, 24 Sep 1997 12:27:53 +0200] rev 3704
sessionK now indexed by nat instead of bool. Weaker Oops conditions on final guarantees
Wed, 24 Sep 1997 12:26:14 +0200 Tidied some proofs using clarify_tac
changeset
paulson [Wed, 24 Sep 1997 12:26:14 +0200] rev 3703
Tidied some proofs using clarify_tac
Wed, 24 Sep 1997 12:25:32 +0200 clarify_tac and a new simprule
changeset
paulson [Wed, 24 Sep 1997 12:25:32 +0200] rev 3702
clarify_tac and a new simprule
Wed, 24 Sep 1997 12:24:41 +0200 Names and saves the theorem parts_spies_subset_used
changeset
paulson [Wed, 24 Sep 1997 12:24:41 +0200] rev 3701
Names and saves the theorem parts_spies_subset_used
Wed, 24 Sep 1997 10:51:52 +0200 pure_trfuns: added constraint;
changeset
wenzelm [Wed, 24 Sep 1997 10:51:52 +0200] rev 3700
pure_trfuns: added constraint;
Tue, 23 Sep 1997 17:35:07 +0200 added handle_error: ('a -> 'b) -> 'a -> 'b error;
changeset
wenzelm [Tue, 23 Sep 1997 17:35:07 +0200] rev 3699
added handle_error: ('a -> 'b) -> 'a -> 'b error;
Tue, 23 Sep 1997 08:44:57 +0200 index.html obsolete;
changeset
wenzelm [Tue, 23 Sep 1997 08:44:57 +0200] rev 3698
index.html obsolete;
Mon, 22 Sep 1997 17:38:55 +0200 Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;
changeset
wenzelm [Mon, 22 Sep 1997 17:38:55 +0200] rev 3697
Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories; HOLCF: fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
Mon, 22 Sep 1997 17:37:48 +0200 acks;
changeset
wenzelm [Mon, 22 Sep 1997 17:37:48 +0200] rev 3696
acks;
Mon, 22 Sep 1997 17:37:24 +0200 added Cambridge fs;
changeset
wenzelm [Mon, 22 Sep 1997 17:37:24 +0200] rev 3695
added Cambridge fs;
Mon, 22 Sep 1997 17:37:03 +0200 fixed pttrn syntax;
changeset
wenzelm [Mon, 22 Sep 1997 17:37:03 +0200] rev 3694
fixed pttrn syntax;
Mon, 22 Sep 1997 17:35:52 +0200 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
changeset
wenzelm [Mon, 22 Sep 1997 17:35:52 +0200] rev 3693
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
Mon, 22 Sep 1997 17:31:57 +0200 tuned pattern syntax;
changeset
wenzelm [Mon, 22 Sep 1997 17:31:57 +0200] rev 3692
tuned pattern syntax;
Mon, 22 Sep 1997 17:31:28 +0200 tuned lambda_ast_tr, idtyp_ast_tr' to accomodate fix of idt/idts
changeset
wenzelm [Mon, 22 Sep 1997 17:31:28 +0200] rev 3691
tuned lambda_ast_tr, idtyp_ast_tr' to accomodate fix of idt/idts vs. pttrn/pttrns;
(0) -3000 -1000 -300 -100 -64 +64 +100 +300 +1000 +3000 +10000 +30000 tip
isabelle