more finalconsts;
authorwenzelm
Thu Sep 29 00:58:55 2005 +0200 (2005-09-29)
changeset 17702ea88ddeafabe
parent 17701 6928771d256e
child 17703 6ec36bad47ea
more finalconsts;
src/FOL/IFOL.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Nat.thy
src/HOL/Set.thy
     1.1 --- a/src/FOL/IFOL.thy	Thu Sep 29 00:58:54 2005 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Thu Sep 29 00:58:55 2005 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4  global
     1.5  
     1.6  classes "term"
     1.7 +final_consts term_class
     1.8  defaultsort "term"
     1.9  
    1.10  typedecl o
     2.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Sep 29 00:58:54 2005 +0200
     2.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Sep 29 00:58:55 2005 +0200
     2.3 @@ -34,6 +34,8 @@
     2.4  
     2.5  axioms
     2.6    someI: "P (x::'a) ==> P (SOME x. P x)"
     2.7 +finalconsts
     2.8 +  Eps
     2.9  
    2.10  
    2.11  constdefs
     3.1 --- a/src/HOL/Nat.thy	Thu Sep 29 00:58:54 2005 +0200
     3.2 +++ b/src/HOL/Nat.thy	Thu Sep 29 00:58:55 2005 +0200
     3.3 @@ -24,7 +24,9 @@
     3.4    -- {* the axiom of infinity in 2 parts *}
     3.5    inj_Suc_Rep:          "inj Suc_Rep"
     3.6    Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
     3.7 -
     3.8 +finalconsts
     3.9 +  Zero_Rep
    3.10 +  Suc_Rep
    3.11  
    3.12  subsection {* Type nat *}
    3.13  
     4.1 --- a/src/HOL/Set.thy	Thu Sep 29 00:58:54 2005 +0200
     4.2 +++ b/src/HOL/Set.thy	Thu Sep 29 00:58:55 2005 +0200
     4.3 @@ -305,6 +305,9 @@
     4.4  axioms
     4.5    mem_Collect_eq: "(a : {x. P(x)}) = P(a)"
     4.6    Collect_mem_eq: "{x. x:A} = A"
     4.7 +finalconsts
     4.8 +  Collect
     4.9 +  "op :"
    4.10  
    4.11  defs
    4.12    Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"