etc/isar-keywords.el
changeset 55476 e2cf2df4fd83
parent 55447 aa41ecbdc205
child 55532 b751e6d7f4e9
     1.1 --- a/etc/isar-keywords.el	Fri Feb 14 10:33:57 2014 +0100
     1.2 +++ b/etc/isar-keywords.el	Fri Feb 14 11:10:28 2014 +0100
     1.3 @@ -80,7 +80,6 @@
     1.4      "done"
     1.5      "enable_pr"
     1.6      "end"
     1.7 -    "enriched_type"
     1.8      "equivariance"
     1.9      "exit"
    1.10      "export_code"
    1.11 @@ -92,11 +91,13 @@
    1.12      "find_unused_assms"
    1.13      "fix"
    1.14      "fixrec"
    1.15 +    "free_constructors"
    1.16      "from"
    1.17      "full_prf"
    1.18      "fun"
    1.19      "fun_cases"
    1.20      "function"
    1.21 +    "functor"
    1.22      "guess"
    1.23      "have"
    1.24      "header"
    1.25 @@ -299,7 +300,6 @@
    1.26      "values_prolog"
    1.27      "welcome"
    1.28      "with"
    1.29 -    "wrap_free_constructors"
    1.30      "write"
    1.31      "{"
    1.32      "}"))
    1.33 @@ -597,8 +597,9 @@
    1.34      "code_pred"
    1.35      "corollary"
    1.36      "cpodef"
    1.37 -    "enriched_type"
    1.38 +    "free_constructors"
    1.39      "function"
    1.40 +    "functor"
    1.41      "instance"
    1.42      "interpretation"
    1.43      "lemma"
    1.44 @@ -621,8 +622,7 @@
    1.45      "sublocale"
    1.46      "termination"
    1.47      "theorem"
    1.48 -    "typedef"
    1.49 -    "wrap_free_constructors"))
    1.50 +    "typedef"))
    1.51  
    1.52  (defconst isar-keywords-qed
    1.53    '("\\."