Mercurial
Mercurial
>
repos
>
isabelle
/ changelog
summary
|
shortlog
| changelog |
graph
|
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
(0)
-300
-100
-30
-10
-3
+3
+10
+30
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
Mon, 28 Nov 1994 19:48:30 +0100
----------------------------------------------------------------------
changeset
regensbu [Mon, 28 Nov 1994 19:48:30 +0100] rev 752
---------------------------------------------------------------------- Committing in HOLCF Use new translation mechanism and keyword syntax, cinfix.ML no longer needed. Optimized proofs in Cont.ML Modified Files: Cfun1.ML Cfun2.thy Cont.ML Cprod3.thy Makefile README Sprod3.thy Tr2.thy ccc1.thy ----------------------------------------------------------------------
Fri, 25 Nov 1994 11:13:55 +0100
ZF/indrule/mutual_ind_tac: ensured that asm_full_simp_tac ignores any
changeset
lcp [Fri, 25 Nov 1994 11:13:55 +0100] rev 751
ZF/indrule/mutual_ind_tac: ensured that asm_full_simp_tac ignores any equalities, by adding setmksimps K[]. ZF/indrule/mut_ss: removed Collect_cong; it is redundant.
Fri, 25 Nov 1994 11:08:12 +0100
checks that the recursive sets are Consts before taking
changeset
lcp [Fri, 25 Nov 1994 11:08:12 +0100] rev 750
checks that the recursive sets are Consts before taking them apart! Bug was introduced during the translation to theory sections.
(0)
-300
-100
-30
-10
-3
+3
+10
+30
+100
+300
+1000
+3000
+10000
+30000
tip