equal
deleted
inserted
replaced
37 |
37 |
38 |
38 |
39 *** FOL *** |
39 *** FOL *** |
40 |
40 |
41 * Added the "at most 1" quantifier, Uniq, as in HOL. |
41 * Added the "at most 1" quantifier, Uniq, as in HOL. |
|
42 |
|
43 * Simproc defined_all and rewrite rules subst_all and subst_all' perform |
|
44 more aggressive substitution with variables from assumptions. |
|
45 INCOMPATIBILITY, use something like |
|
46 "supply subst_all [simp] subst_all' [simp] [[simproc del: defined_all]]" |
|
47 to leave fragile proofs unaffected. |
42 |
48 |
43 |
49 |
44 *** ML *** |
50 *** ML *** |
45 |
51 |
46 * Antiquotations @{scala_function} and @{scala} refer to registered |
52 * Antiquotations @{scala_function} and @{scala} refer to registered |